Theorem 3orbi123d 1301

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 783	. . 3 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	orbi12d 783	. 2 |- ( ph -> ( ( ( ps \/ th ) \/ et ) <-> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or 969	. 2 |- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or 969	. 2 |- ( ( ch \/ ta \/ ze ) <-> ( ( ch \/ ta ) \/ ze ) )
8	5, 6, 7	3bitr4g 222	1 |- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )

Syntax hints:   -> wi 4   <-> wb 104   \/ wo 698   \/ w3o 967

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

This theorem depends on definitions:  df-bi 116  df-3or 969

This theorem is referenced by:  ordtriexmid  4498  ontriexmidim  4499  wetriext  4554  nntri3or  6461  tridc  6865  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  onntri35  7193  ltsopi  7261  pitri3or  7263  nqtri3or  7337  elz  9193  ztri3or  9234  qtri3or  10178  trilpo  13922  trirec0  13923  reap0  13937