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

Theorem 3orbi123d 1251
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 690 . . 3  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
4 bi3d.3 . . 3  |-  ( ph  ->  ( et  <->  ze )
)
53, 4orbi12d 690 . 2  |-  ( ph  ->  ( ( ( ps  \/  th )  \/  et )  <->  ( ( ch  \/  ta )  \/ 
ze ) ) )
6 df-3or 935 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
7 df-3or 935 . 2  |-  ( ( ch  \/  ta  \/  ze )  <->  ( ( ch  \/  ta )  \/ 
ze ) )
85, 6, 73bitr4g 279 1  |-  ( ph  ->  ( ( ps  \/  th  \/  et )  <->  ( ch  \/  ta  \/  ze )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    \/ w3o 933
This theorem is referenced by:  moeq3  2955  soeq1  4349  solin  4353  ordtri3or  4440  dfwe2  4589  soinxp  4770  isosolem  5860  f1oweALT  5867  soxp  6244  sorpssi  6299  elfiun  7199  sornom  7919  ltsopr  8672  elz  10042  dyaddisj  18967  colinearalg  24610  axlowdim2  24660  axlowdim  24661  brcolinear2  24753  colineardim1  24756  colinearperm1  24757  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  sgplpte21  26235  sgplpte21b  26237  sgplpte22  26241  nb3graprlem2  28288  3orbi123  28572
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-3or 935
  Copyright terms: Public domain W3C validator