Metamath Proof Explorer

Theorem com23

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 φ ψ χ θ
Assertion com23 φ χ ψ θ


Step Hyp Ref Expression
1 com3.1 φ ψ χ θ
2 pm2.27 χ χ θ θ
3 1 2 syl9 φ χ ψ θ