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

Theorem orri 376
Description: Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
orri.1
Assertion
Ref Expression
orri

Proof of Theorem orri
StepHypRef Expression
1 orri.1 . 2
2 df-or 370 . 2
31, 2mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  orci  390  olci  391  pm2.25  404  exmid  415  pm2.13  418  pm3.12  500  pm5.11  884  pm5.12  885  pm5.14  886  pm5.15  889  pm5.55  897  pm5.54  902  rb-ax2  1586  rb-ax3  1587  rb-ax4  1588  exmo  2309  axi12  2433  axbnd  2434  exmidne  2662  abvor0  3803  ifeqor  3985  fvbr0  5892  letrii  9730  numclwwlkdisj  25080  tsim2  30538  tsbi3  30542  tsan2  30549  tsan3  30550
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
  Copyright terms: Public domain W3C validator