Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical implication
com23
Metamath Proof Explorer
Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated
with com12 . (Contributed by NM , 27-Dec-1992) (Proof shortened by Wolf Lammen , 4-Aug-2012)

Ref
Expression
Hypothesis
com3.1
$${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$
Assertion
com23
$${\u22a2}{\phi}\to \left({\chi}\to \left({\psi}\to {\theta}\right)\right)$$

Proof
Step
Hyp
Ref
Expression
1
com3.1
$${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$
2
pm2.27
$${\u22a2}{\chi}\to \left(\left({\chi}\to {\theta}\right)\to {\theta}\right)$$
3
1 2
syl9
$${\u22a2}{\phi}\to \left({\chi}\to \left({\psi}\to {\theta}\right)\right)$$