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  4100  eqoreldif  4689  pwpw0  4817  sssn  4830  pwsnOLD  4902  unissint  4977  disjiund  5139  disjxiun  5146  otsndisj  5520  otiunsndisj  5521  pwssun  5572  isso2i  5624  ordtr3  6410  ordtri2or  6463  unizlim  6488  fvclss  7241  orduniorsuc  7818  ordzsl  7834  nn0suc  7886  xpexr  7909  soseq  8145  odi  8579  swoso  8736  erdisj  8755  ordtypelem7  9519  wemapsolem  9545  domwdom  9569  iscard3  10088  ackbij1lem18  10232  fin56  10388  entric  10552  gchdomtri  10624  inttsk  10769  r1tskina  10777  psslinpr  11026  ssxr  11283  letric  11314  mul0or  11854  mulge0b  12084  zeo  12648  uzm1  12860  xrletri  13132  supxrgtmnf  13308  sq01  14188  ruclem3  16176  prm2orodd  16628  phiprmpw  16709  pleval2i  18289  irredn0  20237  drngmul0or  20386  lvecvs0or  20721  lssvs0or  20723  lspsnat  20758  lsppratlem1  20760  domnchr  21084  fctop  22507  cctop  22509  ppttop  22510  clslp  22652  restntr  22686  cnconn  22926  txindis  23138  txconn  23193  isufil2  23412  ufprim  23413  alexsubALTlem3  23553  pmltpc  24967  iundisj2  25066  limcco  25410  fta1b  25687  aalioulem2  25846  abelthlem2  25944  logreclem  26267  dchrfi  26758  2sqb  26935  nosepdmlem  27186  noetasuplem4  27239  sletric  27267  tgbtwnconn1  27826  legov3  27849  coltr  27898  colline  27900  tglowdim2ln  27902  ragflat3  27957  ragperp  27968  lmieu  28035  lmicom  28039  lmimid  28045  numedglnl  28404  nvmul0or  29903  hvmul0or  30278  atomli  31635  atordi  31637  iundisj2f  31821  iundisj2fi  32008  mxidlprm  32586  ssmxidl  32590  qsdrng  32611  zarclssn  32853  signsply0  33562  pthisspthorcycl  34119  cvmsdisj  34261  nepss  34687  dfon2lem6  34760  btwnconn1lem13  35071  wl-exeq  36403  eqvreldisj  37484  lsator0sp  37871  lkreqN  38040  2at0mat0  38396  trlator0  39042  dochkrshp4  40260  dochsat0  40328  lcfl6  40371  rp-fakeimass  42263  frege124d  42512  clsk1independent  42797  mnringmulrcld  42987  pm10.57  43130  icccncfext  44603  fourierdlem70  44892  ichnreuop  46140  uzlidlring  46827  nneop  47212  mo0sn  47500