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

Theorem 3orbi123i 1143
Description: Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
Hypotheses
Ref Expression
bi3.1  |-  ( ph  <->  ps )
bi3.2  |-  ( ch  <->  th )
bi3.3  |-  ( ta  <->  et )
Assertion
Ref Expression
3orbi123i  |-  ( (
ph  \/  ch  \/  ta )  <->  ( ps  \/  th  \/  et ) )

Proof of Theorem 3orbi123i
StepHypRef Expression
1 bi3.1 . . . 4  |-  ( ph  <->  ps )
2 bi3.2 . . . 4  |-  ( ch  <->  th )
31, 2orbi12i 508 . . 3  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4orbi12i 508 . 2  |-  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ( ps  \/  th )  \/  et )
)
6 df-3or 937 . 2  |-  ( (
ph  \/  ch  \/  ta )  <->  ( ( ph  \/  ch )  \/  ta ) )
7 df-3or 937 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
85, 6, 73bitr4i 269 1  |-  ( (
ph  \/  ch  \/  ta )  <->  ( ps  \/  th  \/  et ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358    \/ w3o 935
This theorem is referenced by:  cadcomb  1402  ne3anior  2638  wecmpep  4517  ordon  4705  cnvso  5353  soxp  6397  sorpss  6465  dford2  7510  elxrge02  24019  brtp  25132  dfon2  25174  sltsolem1  25348  axlowdimlem6  25602
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 178  df-or 360  df-3or 937
  Copyright terms: Public domain W3C validator