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

Theorem 3orbi123d 1288
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 966 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
7 df-3or 966 . 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 964
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 966
This theorem is referenced by:  moeq3  3134  soeq1  4658  solin  4662  ordtri3or  4749  soinxp  4901  isosolem  6036  sorpssi  6364  dfwe2  6391  f1oweALT  6559  soxp  6683  elfiun  7678  sornom  8444  ltsopr  9199  elz  10646  dyaddisj  21074  istrkgl  22919  istrkg2d  22920  axtgupdim2  22930  tglngval  22983  tgellng  22985  colcom  22990  colrot1  22991  lncom  23027  lnrot1  23028  lnrot2  23029  ttgval  23119  colinearalg  23154  axlowdim2  23204  axlowdim  23205  elntg  23228  nb3graprlem2  23358  brcolinear2  28087  colineardim1  28090  colinearperm1  28091  fin2so  28413  frgraregorufr0  30642  3orbi123  31213
  Copyright terms: Public domain W3C validator