Metamath Proof Explorer


Theorem com34

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 . Double deduction associated with com12 . (Contributed by NM, 25-Apr-1994)

Ref Expression
Hypothesis com4.1 φ ψ χ θ τ
Assertion com34 φ ψ θ χ τ

Proof

Step Hyp Ref Expression
1 com4.1 φ ψ χ θ τ
2 pm2.04 χ θ τ θ χ τ
3 1 2 syl6 φ ψ θ χ τ