Theorem orrd 864

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

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

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 849

This theorem is referenced by:  orc  868  olc  869  pm2.68  901  pm4.79  1006  19.30  1881  axi12  2706  r19.30  3120  r19.30OLD  3121  sspss  4102  eqoreldif  4685  pwpw0  4813  sssn  4826  unissint  4972  disjiund  5134  disjxiun  5140  otsndisj  5524  otiunsndisj  5525  pwssun  5575  isso2i  5629  ordtr3  6429  ordtri2or  6482  unizlim  6507  fvclss  7261  orduniorsuc  7850  ordzsl  7866  nn0suc  7916  xpexr  7940  soseq  8184  odi  8617  swoso  8779  erdisj  8799  ordtypelem7  9564  wemapsolem  9590  domwdom  9614  iscard3  10133  ackbij1lem18  10276  fin56  10433  entric  10597  gchdomtri  10669  inttsk  10814  r1tskina  10822  psslinpr  11071  ssxr  11330  letric  11361  mul0or  11903  mulge0b  12138  zeo  12704  uzm1  12916  xrletri  13195  supxrgtmnf  13371  sq01  14264  ruclem3  16269  prm2orodd  16728  phiprmpw  16813  pleval2i  18381  irredn0  20423  drngmul0orOLD  20761  lvecvs0or  21110  lssvs0or  21112  lspsnat  21147  lsppratlem1  21149  domnchr  21547  fctop  23011  cctop  23013  ppttop  23014  clslp  23156  restntr  23190  cnconn  23430  txindis  23642  txconn  23697  isufil2  23916  ufprim  23917  alexsubALTlem3  24057  pmltpc  25485  iundisj2  25584  limcco  25928  fta1b  26211  aalioulem2  26375  abelthlem2  26476  logreclem  26805  dchrfi  27299  2sqb  27476  nosepdmlem  27728  noetasuplem4  27781  sletric  27809  muls0ord  28211  tgbtwnconn1  28583  legov3  28606  coltr  28655  colline  28657  tglowdim2ln  28659  ragflat3  28714  ragperp  28725  lmieu  28792  lmicom  28796  lmimid  28802  numedglnl  29161  pthisspthorcycl  29822  nvmul0or  30669  hvmul0or  31044  atomli  32401  atordi  32403  iundisj2f  32603  iundisj2fi  32799  chnind  33001  gsumfs2d  33058  mxidlprm  33498  ssmxidl  33502  qsdrng  33525  zarclssn  33872  signsply0  34566  cvmsdisj  35275  nepss  35718  dfon2lem6  35789  btwnconn1lem13  36100  wl-exeq  37535  eqvreldisj  38615  lsator0sp  39002  lkreqN  39171  2at0mat0  39527  trlator0  40173  dochkrshp4  41391  dochsat0  41459  lcfl6  41502  expeqidd  42360  rp-fakeimass  43525  frege124d  43774  clsk1independent  44059  mnringmulrcld  44247  pm10.57  44390  icccncfext  45902  fourierdlem70  46191  ichnreuop  47459  uzlidlring  48151  nneop  48447  mo0sn  48735