Theorem 3orbi123d 1324

Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	|- ( ph -> ( ps <-> ch ) )
bi3d.2	|- ( ph -> ( th <-> ta ) )
bi3d.3	|- ( ph -> ( et <-> ze ) )

Assertion

Ref	Expression
3orbi123d	|- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )

Proof of Theorem 3orbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2		bi3d.2	. . . 4 |- ( ph -> ( th <-> ta ) )
3	1, 2	orbi12d 795	. . 3 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	orbi12d 795	. 2 |- ( ph -> ( ( ( ps \/ th ) \/ et ) <-> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or 982	. 2 |- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or 982	. 2 |- ( ( ch \/ ta \/ ze ) <-> ( ( ch \/ ta ) \/ ze ) )
8	5, 6, 7	3bitr4g 223	1 |- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 710   \/ w3o 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711

This theorem depends on definitions:  df-bi 117  df-3or 982

This theorem is referenced by:  ordtriexmid  4569  ontriexmidim  4570  wetriext  4625  nntri3or  6579  tridc  6996  exmidontriimlem3  7335  exmidontriimlem4  7336  exmidontriim  7337  onntri35  7349  ltsopi  7433  pitri3or  7435  nqtri3or  7509  elz  9374  ztri3or  9415  qtri3or  10383  trilpo  15986  trirec0  15987  reap0  16001