Metamath Proof Explorer

Theorem or3dir

Description: Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017)

Ref Expression
Assertion or3dir 
|- ( ( ( ph /\ ps /\ ch ) \/ ta ) <-> ( ( ph \/ ta ) /\ ( ps \/ ta ) /\ ( ch \/ ta ) ) )

Proof

Step Hyp Ref Expression
1 or3di 
 |-  ( ( ta \/ ( ph /\ ps /\ ch ) ) <-> ( ( ta \/ ph ) /\ ( ta \/ ps ) /\ ( ta \/ ch ) ) )
2 orcom 
 |-  ( ( ta \/ ( ph /\ ps /\ ch ) ) <-> ( ( ph /\ ps /\ ch ) \/ ta ) )
3 orcom 
 |-  ( ( ta \/ ph ) <-> ( ph \/ ta ) )
4 orcom 
 |-  ( ( ta \/ ps ) <-> ( ps \/ ta ) )
5 orcom 
 |-  ( ( ta \/ ch ) <-> ( ch \/ ta ) )
6 3 4 5 3anbi123i 
 |-  ( ( ( ta \/ ph ) /\ ( ta \/ ps ) /\ ( ta \/ ch ) ) <-> ( ( ph \/ ta ) /\ ( ps \/ ta ) /\ ( ch \/ ta ) ) )
7 1 2 6 3bitr3i 
 |-  ( ( ( ph /\ ps /\ ch ) \/ ta ) <-> ( ( ph \/ ta ) /\ ( ps \/ ta ) /\ ( ch \/ ta ) ) )