Metamath Proof Explorer


Theorem jcab

Description: Distributive law for implication over conjunction. Compare Theorem *4.76 of WhiteheadRussell p. 121. (Contributed by NM, 3-Apr-1994) (Proof shortened by Wolf Lammen, 27-Nov-2013)

Ref Expression
Assertion jcab ( ( 𝜑 → ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝜓𝜒 ) → 𝜓 )
2 1 imim2i ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( 𝜑𝜓 ) )
3 simpr ( ( 𝜓𝜒 ) → 𝜒 )
4 3 imim2i ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( 𝜑𝜒 ) )
5 2 4 jca ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) )
6 pm3.43 ( ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) → ( 𝜑 → ( 𝜓𝜒 ) ) )
7 5 6 impbii ( ( 𝜑 → ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) )