Metamath Proof Explorer


Theorem pm5.31

Description: Theorem *5.31 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm5.31 ( ( 𝜒 ∧ ( 𝜑𝜓 ) ) → ( 𝜑 → ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝜒 ∧ ( 𝜑𝜓 ) ) → ( 𝜑𝜓 ) )
2 simpl ( ( 𝜒 ∧ ( 𝜑𝜓 ) ) → 𝜒 )
3 1 2 jctird ( ( 𝜒 ∧ ( 𝜑𝜓 ) ) → ( 𝜑 → ( 𝜓𝜒 ) ) )