Metamath Proof Explorer

Theorem orddi

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

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

Proof

Step Hyp Ref Expression
1 ordir 
 |-  ( ( ( ph /\ ps ) \/ ( ch /\ th ) ) <-> ( ( ph \/ ( ch /\ th ) ) /\ ( ps \/ ( ch /\ th ) ) ) )
2 ordi 
 |-  ( ( ph \/ ( ch /\ th ) ) <-> ( ( ph \/ ch ) /\ ( ph \/ th ) ) )
3 ordi 
 |-  ( ( ps \/ ( ch /\ th ) ) <-> ( ( ps \/ ch ) /\ ( ps \/ th ) ) )
4 2 3 anbi12i 
 |-  ( ( ( 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 ) ) ) )