Theorem orrd 862

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 851	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

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

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 206  df-or 847

This theorem is referenced by:  orc  866  olc  867  pm2.68  900  pm4.79  1003  19.30  1885  axi12  2702  r19.30  3121  r19.30OLD  3122  sspss  4097  eqoreldif  4684  pwpw0  4812  sssn  4825  pwsnOLD  4897  unissint  4972  disjiund  5134  disjxiun  5141  otsndisj  5515  otiunsndisj  5516  pwssun  5567  isso2i  5619  ordtr3  6401  ordtri2or  6454  unizlim  6479  fvclss  7228  orduniorsuc  7805  ordzsl  7821  nn0suc  7873  xpexr  7896  soseq  8132  odi  8567  swoso  8724  erdisj  8743  ordtypelem7  9506  wemapsolem  9532  domwdom  9556  iscard3  10075  ackbij1lem18  10219  fin56  10375  entric  10539  gchdomtri  10611  inttsk  10756  r1tskina  10764  psslinpr  11013  ssxr  11270  letric  11301  mul0or  11841  mulge0b  12071  zeo  12635  uzm1  12847  xrletri  13119  supxrgtmnf  13295  sq01  14175  ruclem3  16163  prm2orodd  16615  phiprmpw  16696  pleval2i  18276  irredn0  20215  drngmul0or  20321  lvecvs0or  20698  lssvs0or  20700  lspsnat  20735  lsppratlem1  20737  domnchr  21057  fctop  22476  cctop  22478  ppttop  22479  clslp  22621  restntr  22655  cnconn  22895  txindis  23107  txconn  23162  isufil2  23381  ufprim  23382  alexsubALTlem3  23522  pmltpc  24936  iundisj2  25035  limcco  25379  fta1b  25656  aalioulem2  25815  abelthlem2  25913  logreclem  26234  dchrfi  26725  2sqb  26902  nosepdmlem  27153  noetasuplem4  27206  sletric  27234  tgbtwnconn1  27793  legov3  27816  coltr  27865  colline  27867  tglowdim2ln  27869  ragflat3  27924  ragperp  27935  lmieu  28002  lmicom  28006  lmimid  28012  numedglnl  28371  nvmul0or  29868  hvmul0or  30243  atomli  31600  atordi  31602  iundisj2f  31787  iundisj2fi  31979  mxidlprm  32537  ssmxidl  32539  qsdrng  32557  zarclssn  32784  signsply0  33493  pthisspthorcycl  34050  cvmsdisj  34192  nepss  34618  dfon2lem6  34691  btwnconn1lem13  35002  wl-exeq  36308  eqvreldisj  37390  lsator0sp  37777  lkreqN  37946  2at0mat0  38302  trlator0  38948  dochkrshp4  40166  dochsat0  40234  lcfl6  40277  rp-fakeimass  42134  frege124d  42383  clsk1independent  42668  mnringmulrcld  42858  pm10.57  43001  icccncfext  44476  fourierdlem70  44765  ichnreuop  46013  uzlidlring  46667  nneop  47052  mo0sn  47340