$A\land FB\rightarrow F(PA\land B)$ in temporal logic Temporal minimal logic $\mathbf{K_T}$ calculus is characterised by the following axioms, where $F=_{\text{def}} \lnot G\lnot$ and $P=_{\text{def}} \lnot H\lnot$:


*

*$G(A\rightarrow B)\rightarrow (GA\rightarrow GB)$

*$H(A\rightarrow B)\rightarrow (HA\rightarrow HB)$

*$A\rightarrow GPA$

*$A\rightarrow HFA$


and the rules deriving $GA$ and $HA$ from $\vdash A$. The intensional operators can be read as follows: $F$ 'at some instant in the future', $P$ 'at some instant in the past', $G$ 'always in the future' and $H$ 'always in the past'.
I read -D. Palladino, C. Palladino, Logiche non classiche- that the following theorems follows from such a system:$$A\land FB\rightarrow F(PA\land B)$$$$A\land PB\rightarrow P(FA\land B)$$but I cannot prove it, although I think that the symmetry of the operators allows to use an analogous inference pattern for both cases. If we use Kripke semantics to define instants as worlds with a partial order relation $<$, it is easy for me to see how to derive the desired theorems, but I cannot derive them from the $\mathbf{K_T}$ axioms. Could anybody explain how to do so? I thank you very much!!!
 A: Working by contradiction (i.e. starting with the negation of the statement and trying to show that it is a logical falsehood): 
\begin{align}
&\neg\big(A\land FB\to F(PA\land B)\big)\\
\Longleftrightarrow&(A\land FB)\land \neg F(PA\land B)\\
\Longleftrightarrow&(A\land\neg G\neg B)\land G\neg(\neg H\neg A\land B)\qquad\text{(definition F,P)}\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land G(H\neg A\lor\neg B)\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land G(\neg H\neg A\to\neg B)\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (G\neg H\neg A\to G\neg B)\qquad\text{(1)}\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (GPA\to G\neg B)\qquad\text{(definition P)}\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (\neg GPA\lor G\neg B)\\
\Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (\neg A\lor G\neg B)\qquad\text{(contrapositive of 4)}
\end{align}
Clearly the last line is a contradiction, of the form $\psi\land\neg\psi$. Therefore, since the negation of the theorem is false, the theorem itself must be true (tautology).
