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

Theorem 3orbi123d 1334
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 714 . . 3  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4orbi12d 714 . 2  |-  ( ph  ->  ( ( ( ps  \/  th )  \/  et )  <->  ( ( ch  \/  ta )  \/ 
ze ) ) )
6 df-3or 983 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
7 df-3or 983 . 2  |-  ( ( ch  \/  ta  \/  ze )  <->  ( ( ch  \/  ta )  \/ 
ze ) )
85, 6, 73bitr4g 291 1  |-  ( ph  ->  ( ( ps  \/  th  \/  et )  <->  ( ch  \/  ta  \/  ze )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    \/ w3o 981
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 188  df-or 371  df-3or 983
This theorem is referenced by:  moeq3  3248  soeq1  4790  solin  4794  soinxp  4915  ordtri3or  5471  isosolem  6250  sorpssi  6588  dfwe2  6619  f1oweALT  6788  soxp  6917  elfiun  7947  sornom  8708  ltsopr  9458  elz  10940  dyaddisj  22541  istrkgl  24493  istrkgld  24494  axtgupdim2  24506  tgdim01  24538  tglngval  24583  tgellng  24585  colcom  24590  colrot1  24591  legso  24631  lncom  24654  lnrot1  24655  lnrot2  24656  ttgval  24892  colinearalg  24927  axlowdim2  24977  axlowdim  24978  elntg  25001  nb3graprlem2  25166  frgraregorufr0  25766  istrkg2d  29479  axtgupdim2OLD  29481  brcolinear2  30818  colineardim1  30821  colinearperm1  30822  fin2so  31846  3orbi123  36726
  Copyright terms: Public domain W3C validator