Metamath Proof Explorer


Theorem pm4.38

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

Ref Expression
Assertion pm4.38 ( ( ( 𝜑𝜒 ) ∧ ( 𝜓𝜃 ) ) → ( ( 𝜑𝜓 ) ↔ ( 𝜒𝜃 ) ) )

Proof

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