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  1878  axi12  2703  r19.30  3117  r19.30OLD  3118  sspss  4111  eqoreldif  4689  pwpw0  4817  sssn  4830  unissint  4976  disjiund  5138  disjxiun  5144  otsndisj  5528  otiunsndisj  5529  pwssun  5579  isso2i  5632  ordtr3  6430  ordtri2or  6483  unizlim  6508  fvclss  7260  orduniorsuc  7849  ordzsl  7865  nn0suc  7916  xpexr  7940  soseq  8182  odi  8615  swoso  8777  erdisj  8797  ordtypelem7  9561  wemapsolem  9587  domwdom  9611  iscard3  10130  ackbij1lem18  10273  fin56  10430  entric  10594  gchdomtri  10666  inttsk  10811  r1tskina  10819  psslinpr  11068  ssxr  11327  letric  11358  mul0or  11900  mulge0b  12135  zeo  12701  uzm1  12913  xrletri  13191  supxrgtmnf  13367  sq01  14260  ruclem3  16265  prm2orodd  16724  phiprmpw  16809  pleval2i  18393  irredn0  20439  drngmul0orOLD  20777  lvecvs0or  21127  lssvs0or  21129  lspsnat  21164  lsppratlem1  21166  domnchr  21564  fctop  23026  cctop  23028  ppttop  23029  clslp  23171  restntr  23205  cnconn  23445  txindis  23657  txconn  23712  isufil2  23931  ufprim  23932  alexsubALTlem3  24072  pmltpc  25498  iundisj2  25597  limcco  25942  fta1b  26225  aalioulem2  26389  abelthlem2  26490  logreclem  26819  dchrfi  27313  2sqb  27490  nosepdmlem  27742  noetasuplem4  27795  sletric  27823  muls0ord  28225  tgbtwnconn1  28597  legov3  28620  coltr  28669  colline  28671  tglowdim2ln  28673  ragflat3  28728  ragperp  28739  lmieu  28806  lmicom  28810  lmimid  28816  numedglnl  29175  nvmul0or  30678  hvmul0or  31053  atomli  32410  atordi  32412  iundisj2f  32609  iundisj2fi  32804  chnind  32984  gsumfs2d  33040  mxidlprm  33477  ssmxidl  33481  qsdrng  33504  zarclssn  33833  signsply0  34544  pthisspthorcycl  35112  cvmsdisj  35254  nepss  35697  dfon2lem6  35769  btwnconn1lem13  36080  wl-exeq  37514  eqvreldisj  38595  lsator0sp  38982  lkreqN  39151  2at0mat0  39507  trlator0  40153  dochkrshp4  41371  dochsat0  41439  lcfl6  41482  expeqidd  42338  rp-fakeimass  43501  frege124d  43750  clsk1independent  44035  mnringmulrcld  44223  pm10.57  44366  icccncfext  45842  fourierdlem70  46131  ichnreuop  47396  uzlidlring  48078  nneop  48375  mo0sn  48663