Metamath Proof Explorer


Theorem 3com12d

Description: Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009)

Ref Expression
Hypothesis 3com12d.1 ( 𝜑 → ( 𝜓𝜒𝜃 ) )
Assertion 3com12d ( 𝜑 → ( 𝜒𝜓𝜃 ) )

Proof

Step Hyp Ref Expression
1 3com12d.1 ( 𝜑 → ( 𝜓𝜒𝜃 ) )
2 id ( ( 𝜒𝜓𝜃 ) → ( 𝜒𝜓𝜃 ) )
3 2 3com12 ( ( 𝜓𝜒𝜃 ) → ( 𝜒𝜓𝜃 ) )
4 1 3 syl ( 𝜑 → ( 𝜒𝜓𝜃 ) )