Metamath Proof Explorer

Theorem anddi

Description: Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion anddi 
|- ( ( ( ph \/ ps ) /\ ( ch \/ th ) ) <-> ( ( ( ph /\ ch ) \/ ( ph /\ th ) ) \/ ( ( ps /\ ch ) \/ ( ps /\ th ) ) ) )

Proof

Step Hyp Ref Expression
1 andir 
 |-  ( ( ( ph \/ ps ) /\ ( ch \/ th ) ) <-> ( ( ph /\ ( ch \/ th ) ) \/ ( ps /\ ( ch \/ th ) ) ) )
2 andi 
 |-  ( ( ph /\ ( ch \/ th ) ) <-> ( ( ph /\ ch ) \/ ( ph /\ th ) ) )
3 andi 
 |-  ( ( ps /\ ( ch \/ th ) ) <-> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )
4 2 3 orbi12i 
 |-  ( ( ( ph /\ ( ch \/ th ) ) \/ ( ps /\ ( ch \/ th ) ) ) <-> ( ( ( ph /\ ch ) \/ ( ph /\ th ) ) \/ ( ( ps /\ ch ) \/ ( ps /\ th ) ) ) )
5 1 4 bitri 
 |-  ( ( ( ph \/ ps ) /\ ( ch \/ th ) ) <-> ( ( ( ph /\ ch ) \/ ( ph /\ th ) ) \/ ( ( ps /\ ch ) \/ ( ps /\ th ) ) ) )