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

Theorem 3orbi123i 1143
 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 508 . . 3
4 bi3.3 . . 3
53, 4orbi12i 508 . 2
6 df-3or 937 . 2
7 df-3or 937 . 2
85, 6, 73bitr4i 269 1
 Colors of variables: wff set class Syntax hints:   wb 177   wo 358   w3o 935 This theorem is referenced by:  cadcomb  1405  ne3anior  2684  wecmpep  4566  ordon  4755  cnvso  5403  soxp  6451  sorpss  6519  dford2  7565  elxrge02  24168  brtp  25362  dfon2  25407  sltsolem1  25588  axlowdimlem6  25851 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