This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem or3di

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

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

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( ps /\ ch /\ ta ) <-> ( ( ps /\ ch ) /\ ta ) )
2 1 orbi2i 
 |-  ( ( ph \/ ( ps /\ ch /\ ta ) ) <-> ( ph \/ ( ( ps /\ ch ) /\ ta ) ) )
3 ordi 
 |-  ( ( ph \/ ( ( ps /\ ch ) /\ ta ) ) <-> ( ( ph \/ ( ps /\ ch ) ) /\ ( ph \/ ta ) ) )
4 ordi 
 |-  ( ( ph \/ ( ps /\ ch ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) ) )
5 4 anbi1i 
 |-  ( ( ( ph \/ ( ps /\ ch ) ) /\ ( ph \/ ta ) ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ph \/ ta ) ) )
6 2 3 5 3bitri 
 |-  ( ( ph \/ ( ps /\ ch /\ ta ) ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ph \/ ta ) ) )
7 df-3an 
 |-  ( ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ph \/ ta ) ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ph \/ ta ) ) )
8 6 7 bitr4i 
 |-  ( ( ph \/ ( ps /\ ch /\ ta ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ph \/ ta ) ) )