Theorem orrd 877

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orc  881  olc  882  pm2.68  914  pm4.79  1021  19.30  1914  axi12  2731  r19.30  3130  sspss  4050  eqoreldif  4646  pwpw0  4774  sssn  4787  unissint  4932  disjiund  5094  disjxiun  5100  otsndisj  5492  otiunsndisj  5493  pwssun  5543  isso2i  5596  ordtr3  6402  ordtri2or  6456  unizlim  6480  fvclss  7237  orduniorsuc  7830  ordzsl  7845  nn0suc  7895  xpexr  7919  soseq  8160  odi  8571  swoso  8736  erdisj  8759  ordtypelem7  9502  wemapsolem  9528  domwdom  9552  iscard3  10153  ackbij1lem18  10295  fin56  10452  entric  10622  gchdomtri  10695  inttsk  10840  r1tskina  10848  psslinpr  11097  1re  11289  ssxr  11360  letric  11391  mul0or  11937  mulge0b  12168  zeo  12766  uzm1  12980  xrletri  13263  supxrgtmnf  13440  sq01  14349  ruclem3  16381  prm2orodd  16846  phiprmpw  16933  pleval2i  18488  chnind  18775  irredn0  20633  lvecvs0or  21366  lssvs0or  21368  lspsnat  21403  lsppratlem1  21405  domnchr  21818  fctop  23302  cctop  23304  ppttop  23305  clslp  23446  restntr  23480  cnconn  23720  txindis  23933  txconn  23988  isufil2  24207  ufprim  24208  alexsubALTlem3  24348  pmltpc  25751  iundisj2  25850  limcco  26193  fta1b  26470  aalioulem2  26642  abelthlem2  26741  logreclem  27072  dchrfi  27564  2sqb  27741  nosepdmlem  28022  noetasuplem4  28075  lestric  28107  muls0ord  28553  bdayfinbndlem1  28835  tgbtwnconn1  29020  legov3  29043  coltr  29098  colline  29100  tglowdim2ln  29102  ragflat3  29163  ragperp  29174  lmieu  29271  lmicom  29275  lmimid  29281  numedglnl  29704  pthisspthorcycl  30372  nvmul0or  31234  hvmul0or  31609  atomli  32966  atordi  32968  iundisj2f  33166  iundisj2fi  33371  gsumfs2d  33604  mxidlprm  33977  ssmxidl  33981  qsdrng  34003  dflringlem3  34010  dflring4  34012  zarclssn  34487  signsply0  35163  cvmsdisj  36004  nepss  36452  dfon2lem6  36520  btwnconn1lem13  36834  wl-exeq  38434  eqvreldisj  39598  lsator0sp  40026  lkreqN  40195  2at0mat0  40550  trlator0  41196  dochkrshp4  42414  dochsat0  42482  lcfl6  42525  expeqidd  43350  sn-remul0ord  43427  rp-fakeimass  44471  frege124d  44720  clsk1independent  45005  mnringmulrcld  45185  pm10.57  45314  icccncfext  46841  fourierdlem70  47130  ichnreuop  48498  uzlidlring  49276  nneop  49582  mo0sn  49870  euendfunc2  50579