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

Theorem 3orbi123d 1298
Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1
bi3d.2
bi3d.3
Assertion
Ref Expression
3orbi123d

Proof of Theorem 3orbi123d
StepHypRef Expression
1 bi3d.1 . . . 4
2 bi3d.2 . . . 4
31, 2orbi12d 709 . . 3
4 bi3d.3 . . 3
53, 4orbi12d 709 . 2
6 df-3or 974 . 2
7 df-3or 974 . 2
85, 6, 73bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368  \/w3o 972
This theorem is referenced by:  moeq3  3276  soeq1  4824  solin  4828  ordtri3or  4915  soinxp  5069  isosolem  6243  sorpssi  6586  dfwe2  6617  f1oweALT  6784  soxp  6913  elfiun  7910  sornom  8678  ltsopr  9431  elz  10891  dyaddisj  22005  istrkgl  23855  istrkg2d  23856  istrkgld  23857  axtgupdim2  23869  tgdim01  23898  tglngval  23938  tgellng  23940  colcom  23945  colrot1  23946  legso  23985  lncom  24002  lnrot1  24003  lnrot2  24004  ttgval  24178  colinearalg  24213  axlowdim2  24263  axlowdim  24264  elntg  24287  nb3graprlem2  24452  frgraregorufr0  25052  brcolinear2  29708  colineardim1  29711  colinearperm1  29712  fin2so  30040  3orbi123  33281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-3or 974
  Copyright terms: Public domain W3C validator