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  1882  axi12  2706  r19.30  3103  sspss  4054  eqoreldif  4642  pwpw0  4769  sssn  4782  unissint  4927  disjiund  5089  disjxiun  5095  otsndisj  5467  otiunsndisj  5468  pwssun  5516  isso2i  5569  ordtr3  6363  ordtri2or  6417  unizlim  6441  fvclss  7187  orduniorsuc  7772  ordzsl  7787  nn0suc  7836  xpexr  7860  soseq  8101  odi  8506  swoso  8669  erdisj  8692  ordtypelem7  9429  wemapsolem  9455  domwdom  9479  iscard3  10003  ackbij1lem18  10146  fin56  10303  entric  10467  gchdomtri  10540  inttsk  10685  r1tskina  10693  psslinpr  10942  1re  11132  ssxr  11202  letric  11233  mul0or  11777  mulge0b  12012  zeo  12578  uzm1  12785  xrletri  13067  supxrgtmnf  13244  sq01  14148  ruclem3  16158  prm2orodd  16618  phiprmpw  16703  pleval2i  18257  chnind  18544  irredn0  20359  drngmul0orOLD  20694  lvecvs0or  21063  lssvs0or  21065  lspsnat  21100  lsppratlem1  21102  domnchr  21487  fctop  22948  cctop  22950  ppttop  22951  clslp  23092  restntr  23126  cnconn  23366  txindis  23578  txconn  23633  isufil2  23852  ufprim  23853  alexsubALTlem3  23993  pmltpc  25407  iundisj2  25506  limcco  25850  fta1b  26133  aalioulem2  26297  abelthlem2  26398  logreclem  26728  dchrfi  27222  2sqb  27399  nosepdmlem  27651  noetasuplem4  27704  lestric  27736  muls0ord  28181  bdayfinbndlem1  28463  tgbtwnconn1  28647  legov3  28670  coltr  28719  colline  28721  tglowdim2ln  28723  ragflat3  28778  ragperp  28789  lmieu  28856  lmicom  28860  lmimid  28866  numedglnl  29217  pthisspthorcycl  29875  nvmul0or  30725  hvmul0or  31100  atomli  32457  atordi  32459  iundisj2f  32665  iundisj2fi  32877  gsumfs2d  33144  mxidlprm  33551  ssmxidl  33555  qsdrng  33578  zarclssn  34030  signsply0  34708  cvmsdisj  35464  nepss  35912  dfon2lem6  35980  btwnconn1lem13  36293  wl-exeq  37739  eqvreldisj  38871  lsator0sp  39261  lkreqN  39430  2at0mat0  39785  trlator0  40431  dochkrshp4  41649  dochsat0  41717  lcfl6  41760  expeqidd  42580  sn-remul0ord  42663  rp-fakeimass  43753  frege124d  44002  clsk1independent  44287  mnringmulrcld  44469  pm10.57  44612  icccncfext  46131  fourierdlem70  46420  ichnreuop  47718  uzlidlring  48481  nneop  48772  mo0sn  49061  euendfunc2  49772