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 206  df-or 845

This theorem is referenced by:  orc  864  olc  865  pm2.68  898  pm4.79  1001  19.30  1881  axi12  2704  r19.30  3117  r19.30OLD  3118  sspss  4033  eqoreldif  4619  pwpw0  4745  sssn  4758  pwsnOLD  4831  unissint  4902  disjiund  5063  disjxiun  5070  otsndisj  5432  otiunsndisj  5433  pwssun  5484  isso2i  5537  ordtr3  6313  ordtri2or  6363  unizlim  6385  fvclss  7122  orduniorsuc  7684  ordzsl  7699  nn0suc  7749  xpexr  7772  odi  8417  swoso  8538  erdisj  8557  ordtypelem7  9290  wemapsolem  9316  domwdom  9340  iscard3  9856  ackbij1lem18  10000  fin56  10156  entric  10320  gchdomtri  10392  inttsk  10537  r1tskina  10545  psslinpr  10794  ssxr  11051  letric  11082  mul0or  11622  mulge0b  11852  zeo  12413  uzm1  12623  xrletri  12894  supxrgtmnf  13070  sq01  13947  ruclem3  15949  prm2orodd  16403  phiprmpw  16484  pleval2i  18061  irredn0  19952  drngmul0or  20019  lvecvs0or  20377  lssvs0or  20379  lspsnat  20414  lsppratlem1  20416  domnchr  20743  fctop  22161  cctop  22163  ppttop  22164  clslp  22306  restntr  22340  cnconn  22580  txindis  22792  txconn  22847  isufil2  23066  ufprim  23067  alexsubALTlem3  23207  pmltpc  24621  iundisj2  24720  limcco  25064  fta1b  25341  aalioulem2  25500  abelthlem2  25598  logreclem  25919  dchrfi  26410  2sqb  26587  tgbtwnconn1  26943  legov3  26966  coltr  27015  colline  27017  tglowdim2ln  27019  ragflat3  27074  ragperp  27085  lmieu  27152  lmicom  27156  lmimid  27162  numedglnl  27521  nvmul0or  29019  hvmul0or  29394  atomli  30751  atordi  30753  iundisj2f  30936  iundisj2fi  31125  mxidlprm  31647  ssmxidl  31649  zarclssn  31830  signsply0  32537  pthisspthorcycl  33097  cvmsdisj  33239  nepss  33669  dfon2lem6  33771  soseq  33810  nosepdmlem  33893  noetasuplem4  33946  btwnconn1lem13  34408  wl-exeq  35700  eqvreldisj  36732  lsator0sp  37020  lkreqN  37189  2at0mat0  37544  trlator0  38190  dochkrshp4  39408  dochsat0  39476  lcfl6  39519  rp-fakeimass  41124  frege124d  41374  clsk1independent  41661  mnringmulrcld  41851  pm10.57  41994  icccncfext  43444  fourierdlem70  43733  ichnreuop  44945  uzlidlring  45508  nneop  45893  mo0sn  46182