Theorem 3orbi123d 1322

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 794	. . 3 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	orbi12d 794	. 2 |- ( ph -> ( ( ( ps \/ th ) \/ et ) <-> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or 981	. 2 |- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or 981	. 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 709   \/ w3o 979

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 710

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

This theorem is referenced by:  ordtriexmid  4535  ontriexmidim  4536  wetriext  4591  nntri3or  6512  tridc  6917  exmidontriimlem3  7241  exmidontriimlem4  7242  exmidontriim  7243  onntri35  7255  ltsopi  7338  pitri3or  7340  nqtri3or  7414  elz  9274  ztri3or  9315  qtri3or  10262  trilpo  15195  trirec0  15196  reap0  15210