MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3orbi123d Structured version   Unicode version

Theorem 3orbi123d 1298
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
StepHypRef Expression
1 bi3d.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi3d.2 . . . 4  |-  ( ph  ->  ( th  <->  ta )
)
31, 2orbi12d 709 . . 3  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4orbi12d 709 . 2  |-  ( ph  ->  ( ( ( ps  \/  th )  \/  et )  <->  ( ( ch  \/  ta )  \/ 
ze ) ) )
6 df-3or 974 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
7 df-3or 974 . 2  |-  ( ( ch  \/  ta  \/  ze )  <->  ( ( ch  \/  ta )  \/ 
ze ) )
85, 6, 73bitr4g 288 1  |-  ( ph  ->  ( ( ps  \/  th  \/  et )  <->  ( ch  \/  ta  \/  ze )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    \/ w3o 972
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 185  df-or 370  df-3or 974
This theorem is referenced by:  moeq3  3280  soeq1  4819  solin  4823  ordtri3or  4910  soinxp  5064  isosolem  6231  sorpssi  6570  dfwe2  6601  f1oweALT  6768  soxp  6896  elfiun  7890  sornom  8657  ltsopr  9410  elz  10866  dyaddisj  21768  istrkgl  23611  istrkg2d  23612  istrkgld  23613  axtgupdim2  23625  tgdim01  23654  tglngval  23694  tgellng  23696  colcom  23701  colrot1  23702  legso  23740  lncom  23744  lnrot1  23745  lnrot2  23746  ttgval  23882  colinearalg  23917  axlowdim2  23967  axlowdim  23968  elntg  23991  nb3graprlem2  24156  frgraregorufr0  24757  brcolinear2  29313  colineardim1  29316  colinearperm1  29317  fin2so  29645  3orbi123  32378
  Copyright terms: Public domain W3C validator