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 φψχφψφχ