Metamath Proof Explorer


Theorem an13s

Description: Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006)

Ref Expression
Hypothesis an12s.1 φψχθ
Assertion an13s χψφθ

Proof

Step Hyp Ref Expression
1 an12s.1 φψχθ
2 1 exp32 φψχθ
3 2 com13 χψφθ
4 3 imp32 χψφθ