Theorem orrd 863

Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)

Hypothesis

Ref	Expression
orrd.1	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
orrd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orrd

Step	Hyp	Ref	Expression
1		orrd.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2		pm2.54 852	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orc  867  olc  868  pm2.68  900  pm4.79  1005  19.30  1881  axi12  2699  r19.30  3096  sspss  4055  eqoreldif  4639  pwpw0  4767  sssn  4780  unissint  4925  disjiund  5086  disjxiun  5092  otsndisj  5466  otiunsndisj  5467  pwssun  5515  isso2i  5568  ordtr3  6357  ordtri2or  6411  unizlim  6435  fvclss  7181  orduniorsuc  7769  ordzsl  7785  nn0suc  7834  xpexr  7858  soseq  8099  odi  8504  swoso  8666  erdisj  8689  ordtypelem7  9435  wemapsolem  9461  domwdom  9485  iscard3  10006  ackbij1lem18  10149  fin56  10306  entric  10470  gchdomtri  10542  inttsk  10687  r1tskina  10695  psslinpr  10944  1re  11134  ssxr  11203  letric  11234  mul0or  11778  mulge0b  12013  zeo  12580  uzm1  12791  xrletri  13073  supxrgtmnf  13249  sq01  14150  ruclem3  16160  prm2orodd  16620  phiprmpw  16705  pleval2i  18258  irredn0  20326  drngmul0orOLD  20664  lvecvs0or  21033  lssvs0or  21035  lspsnat  21070  lsppratlem1  21072  domnchr  21457  fctop  22907  cctop  22909  ppttop  22910  clslp  23051  restntr  23085  cnconn  23325  txindis  23537  txconn  23592  isufil2  23811  ufprim  23812  alexsubALTlem3  23952  pmltpc  25367  iundisj2  25466  limcco  25810  fta1b  26093  aalioulem2  26257  abelthlem2  26358  logreclem  26688  dchrfi  27182  2sqb  27359  nosepdmlem  27611  noetasuplem4  27664  sletric  27692  muls0ord  28111  tgbtwnconn1  28538  legov3  28561  coltr  28610  colline  28612  tglowdim2ln  28614  ragflat3  28669  ragperp  28680  lmieu  28747  lmicom  28751  lmimid  28757  numedglnl  29107  pthisspthorcycl  29765  nvmul0or  30612  hvmul0or  30987  atomli  32344  atordi  32346  iundisj2f  32552  iundisj2fi  32753  chnind  32966  gsumfs2d  33021  mxidlprm  33420  ssmxidl  33424  qsdrng  33447  zarclssn  33842  signsply0  34521  cvmsdisj  35245  nepss  35693  dfon2lem6  35764  btwnconn1lem13  36075  wl-exeq  37510  eqvreldisj  38593  lsator0sp  38982  lkreqN  39151  2at0mat0  39507  trlator0  40153  dochkrshp4  41371  dochsat0  41439  lcfl6  41482  expeqidd  42301  sn-remul0ord  42384  rp-fakeimass  43488  frege124d  43737  clsk1independent  44022  mnringmulrcld  44204  pm10.57  44347  icccncfext  45872  fourierdlem70  46161  ichnreuop  47460  uzlidlring  48223  nneop  48515  mo0sn  48804  euendfunc2  49516