Metamath Proof Explorer

Theorem andi3or

Description: Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 andi 
 |-  ( ( ph /\ ( ( ps \/ ch ) \/ th ) ) <-> ( ( ph /\ ( ps \/ ch ) ) \/ ( ph /\ th ) ) )
2 andi 
 |-  ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3 2 orbi1i 
 |-  ( ( ( ph /\ ( ps \/ ch ) ) \/ ( ph /\ th ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( ph /\ th ) ) )
4 1 3 bitri 
 |-  ( ( ph /\ ( ( ps \/ ch ) \/ th ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( ph /\ th ) ) )
5 df-3or 
 |-  ( ( ps \/ ch \/ th ) <-> ( ( ps \/ ch ) \/ th ) )
6 5 anbi2i 
 |-  ( ( ph /\ ( ps \/ ch \/ th ) ) <-> ( ph /\ ( ( ps \/ ch ) \/ th ) ) )
7 df-3or 
 |-  ( ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ph /\ th ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( ph /\ th ) ) )
8 4 6 7 3bitr4i 
 |-  ( ( ph /\ ( ps \/ ch \/ th ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ph /\ th ) ) )