Theorem orrd 876

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

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

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 210  df-or 861

This theorem is referenced by:  orc  880  olc  881  pm2.68  913  pm4.79  1021  19.30  1911  axi12  2733  r19.30  3132  sspss  4057  eqoreldif  4652  pwpw0  4780  sssn  4793  unissint  4938  disjiund  5101  disjxiun  5107  otsndisj  5504  otiunsndisj  5505  pwssun  5555  isso2i  5608  ordtr3  6409  ordtri2or  6463  unizlim  6487  fvclss  7241  orduniorsuc  7827  ordzsl  7842  nn0suc  7892  xpexr  7916  soseq  8156  odi  8565  swoso  8730  erdisj  8753  ordtypelem7  9487  wemapsolem  9513  domwdom  9537  iscard3  10078  ackbij1lem18  10220  fin56  10378  entric  10542  gchdomtri  10615  inttsk  10760  r1tskina  10768  psslinpr  11017  1re  11209  ssxr  11280  letric  11311  mul0or  11855  mulge0b  12086  zeo  12683  uzm1  12897  xrletri  13179  supxrgtmnf  13356  sq01  14263  ruclem3  16290  prm2orodd  16750  phiprmpw  16836  pleval2i  18391  chnind  18678  irredn0  20506  lvecvs0or  21213  lssvs0or  21215  lspsnat  21250  lsppratlem1  21252  domnchr  21663  fctop  23142  cctop  23144  ppttop  23145  clslp  23286  restntr  23320  cnconn  23560  txindis  23772  txconn  23827  isufil2  24046  ufprim  24047  alexsubALTlem3  24187  pmltpc  25590  iundisj2  25689  limcco  26033  fta1b  26310  aalioulem2  26477  abelthlem2  26576  logreclem  26908  dchrfi  27400  2sqb  27577  nosepdmlem  27828  noetasuplem4  27881  lestric  27913  muls0ord  28359  bdayfinbndlem1  28641  tgbtwnconn1  28825  legov3  28848  coltr  28902  colline  28904  tglowdim2ln  28906  ragflat3  28967  ragperp  28978  lmieu  29074  lmicom  29078  lmimid  29084  numedglnl  29475  pthisspthorcycl  30132  nvmul0or  30983  hvmul0or  31358  atomli  32715  atordi  32717  iundisj2f  32916  iundisj2fi  33123  gsumfs2d  33362  mxidlprm  33734  ssmxidl  33738  qsdrng  33760  dflringlem3  33767  dflring4  33769  zarclssn  34244  signsply0  34919  cvmsdisj  35743  nepss  36191  dfon2lem6  36259  btwnconn1lem13  36572  wl-exeq  38170  eqvreldisj  39328  lsator0sp  39756  lkreqN  39925  2at0mat0  40280  trlator0  40926  dochkrshp4  42144  dochsat0  42212  lcfl6  42255  expeqidd  43067  sn-remul0ord  43150  rp-fakeimass  44221  frege124d  44470  clsk1independent  44755  mnringmulrcld  44935  pm10.57  45064  icccncfext  46584  fourierdlem70  46873  ichnreuop  48204  uzlidlring  48983  nneop  49289  mo0sn  49577  euendfunc2  50288