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  1882  axi12  2701  r19.30  3099  sspss  4052  eqoreldif  4638  pwpw0  4765  sssn  4778  unissint  4922  disjiund  5082  disjxiun  5088  otsndisj  5459  otiunsndisj  5460  pwssun  5508  isso2i  5561  ordtr3  6352  ordtri2or  6406  unizlim  6430  fvclss  7175  orduniorsuc  7760  ordzsl  7775  nn0suc  7824  xpexr  7848  soseq  8089  odi  8494  swoso  8656  erdisj  8679  ordtypelem7  9410  wemapsolem  9436  domwdom  9460  iscard3  9984  ackbij1lem18  10127  fin56  10284  entric  10448  gchdomtri  10520  inttsk  10665  r1tskina  10673  psslinpr  10922  1re  11112  ssxr  11182  letric  11213  mul0or  11757  mulge0b  11992  zeo  12559  uzm1  12770  xrletri  13052  supxrgtmnf  13228  sq01  14132  ruclem3  16142  prm2orodd  16602  phiprmpw  16687  pleval2i  18240  chnind  18527  irredn0  20342  drngmul0orOLD  20677  lvecvs0or  21046  lssvs0or  21048  lspsnat  21083  lsppratlem1  21085  domnchr  21470  fctop  22920  cctop  22922  ppttop  22923  clslp  23064  restntr  23098  cnconn  23338  txindis  23550  txconn  23605  isufil2  23824  ufprim  23825  alexsubALTlem3  23965  pmltpc  25379  iundisj2  25478  limcco  25822  fta1b  26105  aalioulem2  26269  abelthlem2  26370  logreclem  26700  dchrfi  27194  2sqb  27371  nosepdmlem  27623  noetasuplem4  27676  sletric  27704  muls0ord  28125  tgbtwnconn1  28554  legov3  28577  coltr  28626  colline  28628  tglowdim2ln  28630  ragflat3  28685  ragperp  28696  lmieu  28763  lmicom  28767  lmimid  28773  numedglnl  29123  pthisspthorcycl  29781  nvmul0or  30628  hvmul0or  31003  atomli  32360  atordi  32362  iundisj2f  32568  iundisj2fi  32777  gsumfs2d  33033  mxidlprm  33433  ssmxidl  33437  qsdrng  33460  zarclssn  33884  signsply0  34562  cvmsdisj  35312  nepss  35760  dfon2lem6  35828  btwnconn1lem13  36139  wl-exeq  37574  eqvreldisj  38657  lsator0sp  39046  lkreqN  39215  2at0mat0  39570  trlator0  40216  dochkrshp4  41434  dochsat0  41502  lcfl6  41545  expeqidd  42364  sn-remul0ord  42447  rp-fakeimass  43551  frege124d  43800  clsk1independent  44085  mnringmulrcld  44267  pm10.57  44410  icccncfext  45931  fourierdlem70  46220  ichnreuop  47509  uzlidlring  48272  nneop  48564  mo0sn  48853  euendfunc2  49565