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
bi3.2
bi3.3
Assertion
Ref Expression
3orbi123i

Proof of Theorem 3orbi123i
StepHypRef Expression
1 bi3.1 . . . 4
2 bi3.2 . . . 4
31, 2orbi12i 507 . . 3
4 bi3.3 . . 3
53, 4orbi12i 507 . 2
6 df-3or 935 . 2
7 df-3or 935 . 2
85, 6, 73bitr4i 268 1
 Colors of variables: wff set class Syntax hints:   wb 176   wo 357   w3o 933 This theorem is referenced by:  cadcomb  1386  ne3anior  2545  wecmpep  4401  ordon  4590  cnvso  5230  soxp  6244  sorpss  6298  dford2  7337  elxrge02  23132  brtp  24177  dfon2  24219  sltsolem1  24393  axlowdimlem6  24647  anddi2  25044 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