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

Theorem 3orbi123i 1141
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 507 . . 3  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
4 bi3.3 . . 3  |-  ( ta  <->  et )
53, 4orbi12i 507 . 2  |-  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ( ps  \/  th )  \/  et )
)
6 df-3or 935 . 2  |-  ( (
ph  \/  ch  \/  ta )  <->  ( ( ph  \/  ch )  \/  ta ) )
7 df-3or 935 . 2  |-  ( ( ps  \/  th  \/  et )  <->  ( ( ps  \/  th )  \/  et ) )
85, 6, 73bitr4i 268 1  |-  ( (
ph  \/  ch  \/  ta )  <->  ( ps  \/  th  \/  et ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    \/ w3o 933
This theorem is referenced by:  cadcomb  1386  ne3anior  2532  wecmpep  4385  ordon  4574  cnvso  5214  soxp  6228  sorpss  6282  dford2  7321  elxrge02  23116  brtp  24106  dfon2  24148  sltsolem1  24322  axlowdimlem6  24575  anddi2  24941
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