Metamath Proof Explorer


Theorem 3imp21

Description: The importation inference 3imp with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016) (Revised to shorten 3com12 by Wolf Lammen, 23-Jun-2022.)

Ref Expression
Hypothesis 3imp.1 φ ψ χ θ
Assertion 3imp21 ψ φ χ θ

Proof

Step Hyp Ref Expression
1 3imp.1 φ ψ χ θ
2 1 com13 χ ψ φ θ
3 2 3imp231 ψ φ χ θ