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

Theorem 3orbi123d 1296
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 707 . . 3  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4orbi12d 707 . 2  |-  ( ph  ->  ( ( ( ps  \/  th )  \/  et )  <->  ( ( ch  \/  ta )  \/ 
ze ) ) )
6 df-3or 972 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
7 df-3or 972 . 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 366    \/ w3o 970
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 368  df-3or 972
This theorem is referenced by:  moeq3  3273  soeq1  4808  solin  4812  ordtri3or  4899  soinxp  5053  isosolem  6218  sorpssi  6559  dfwe2  6590  f1oweALT  6757  soxp  6886  elfiun  7882  sornom  8648  ltsopr  9399  elz  10862  dyaddisj  22171  istrkgl  24053  istrkg2d  24054  istrkgld  24055  axtgupdim2  24067  tgdim01  24099  tglngval  24139  tgellng  24141  colcom  24146  colrot1  24147  legso  24186  lncom  24203  lnrot1  24204  lnrot2  24205  ttgval  24380  colinearalg  24415  axlowdim2  24465  axlowdim  24466  elntg  24489  nb3graprlem2  24654  frgraregorufr0  25254  brcolinear2  29936  colineardim1  29939  colinearperm1  29940  fin2so  30280  3orbi123  33668
  Copyright terms: Public domain W3C validator