Theorem orrd 860

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

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

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 845

This theorem is referenced by:  orc  864  olc  865  pm2.68  898  pm4.79  1001  19.30  1882  axi12  2727  r19.30  3258  sspss  4007  eqoreldif  4582  pwpw0  4706  sssn  4719  pwsnOLD  4794  unissint  4865  disjiund  5026  disjxiun  5033  otsndisj  5382  otiunsndisj  5383  pwssun  5430  isso2i  5481  ordtr3  6219  ordtri2or  6269  unizlim  6291  fvclss  6999  orduniorsuc  7550  ordzsl  7565  nn0suc  7611  xpexr  7634  odi  8221  swoso  8338  erdisj  8357  ordtypelem7  9034  wemapsolem  9060  domwdom  9084  iscard3  9566  ackbij1lem18  9710  fin56  9866  entric  10030  gchdomtri  10102  inttsk  10247  r1tskina  10255  psslinpr  10504  ssxr  10761  letric  10791  mul0or  11331  mulge0b  11561  zeo  12120  uzm1  12329  xrletri  12600  supxrgtmnf  12776  sq01  13649  ruclem3  15647  prm2orodd  16101  phiprmpw  16182  pleval2i  17654  irredn0  19538  drngmul0or  19605  lvecvs0or  19962  lssvs0or  19964  lspsnat  19999  lsppratlem1  20001  domnchr  20314  fctop  21718  cctop  21720  ppttop  21721  clslp  21862  restntr  21896  cnconn  22136  txindis  22348  txconn  22403  isufil2  22622  ufprim  22623  alexsubALTlem3  22763  pmltpc  24164  iundisj2  24263  limcco  24606  fta1b  24883  aalioulem2  25042  abelthlem2  25140  logreclem  25461  dchrfi  25952  2sqb  26129  tgbtwnconn1  26482  legov3  26505  coltr  26554  colline  26556  tglowdim2ln  26558  ragflat3  26613  ragperp  26624  lmieu  26691  lmicom  26695  lmimid  26701  numedglnl  27050  nvmul0or  28546  hvmul0or  28921  atomli  30278  atordi  30280  iundisj2f  30465  iundisj2fi  30655  mxidlprm  31174  ssmxidl  31176  zarclssn  31357  signsply0  32062  pthisspthorcycl  32619  cvmsdisj  32761  nepss  33193  dfon2lem6  33293  soseq  33371  nosepdmlem  33484  noetasuplem4  33537  btwnconn1lem13  33985  wl-exeq  35254  eqvreldisj  36324  lsator0sp  36612  lkreqN  36781  2at0mat0  37136  trlator0  37782  dochkrshp4  39000  dochsat0  39068  lcfl6  39111  rp-fakeimass  40638  frege124d  40880  clsk1independent  41167  mnringmulrcld  41354  pm10.57  41493  icccncfext  42940  fourierdlem70  43229  ichnreuop  44416  uzlidlring  44979  nneop  45364