Metamath Proof Explorer


Theorem andi

Description: Distributive law for conjunction. Theorem *4.4 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 5-Jan-2013)

Ref Expression
Assertion andi ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 orc ( ( 𝜑𝜓 ) → ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )
2 olc ( ( 𝜑𝜒 ) → ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )
3 1 2 jaodan ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) → ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )
4 orc ( 𝜓 → ( 𝜓𝜒 ) )
5 4 anim2i ( ( 𝜑𝜓 ) → ( 𝜑 ∧ ( 𝜓𝜒 ) ) )
6 olc ( 𝜒 → ( 𝜓𝜒 ) )
7 6 anim2i ( ( 𝜑𝜒 ) → ( 𝜑 ∧ ( 𝜓𝜒 ) ) )
8 5 7 jaoi ( ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) → ( 𝜑 ∧ ( 𝜓𝜒 ) ) )
9 3 8 impbii ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )