Theorem 3orbi123d 1398

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

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   \/ w3o 1036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-3or 1038

This theorem is referenced by:  moeq3  3383  soeq1  5054  solin  5058  soinxp  5183  ordtri3or  5755  isosolem  6597  sorpssi  6943  dfwe2  6981  f1oweALT  7152  soxp  7290  elfiun  8336  sornom  9099  ltsopr  9854  elz  11379  dyaddisj  23364  istrkgl  25357  istrkgld  25358  axtgupdim2  25370  tgdim01  25402  tglngval  25446  tgellng  25448  colcom  25453  colrot1  25454  legso  25494  lncom  25517  lnrot1  25518  lnrot2  25519  ttgval  25755  colinearalg  25790  axlowdim2  25840  axlowdim  25841  elntg  25864  nb3grprlem2  26283  frgrwopreg  27187  istrkg2d  30744  axtgupdim2OLD  30746  brcolinear2  32165  colineardim1  32168  colinearperm1  32169  fin2so  33396  uneqsn  38321  3orbi123  38717