Theorem 3orbi123d 1352

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 805	. . 3 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	orbi12d 805	. 2 |- ( ph -> ( ( ( ps \/ th ) \/ et ) <-> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or 1010	. 2 |- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or 1010	. 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 720   \/ w3o 1008

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 721

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

This theorem is referenced by:  ordtriexmid  4663  ontriexmidim  4664  wetriext  4719  nntri3or  6756  tridc  7194  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  onntri35  7586  ltsopi  7677  pitri3or  7679  nqtri3or  7753  elz  9625  ztri3or  9666  qtri3or  10653  trilpo  16997  trirec0  16998  reap0  17013