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  2942  soeq1  4333  solin  4337  ordtri3or  4424  dfwe2  4573  soinxp  4754  isosolem  5844  f1oweALT  5851  soxp  6228  sorpssi  6283  elfiun  7183  sornom  7903  ltsopr  8656  elz  10026  dyaddisj  18951  colinearalg  24538  axlowdim2  24588  axlowdim  24589  brcolinear2  24681  colineardim1  24684  colinearperm1  24685  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  sgplpte21  26132  sgplpte21b  26134  sgplpte22  26138  3orbi123  28273
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