Theorem orrd 862

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

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

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 847

This theorem is referenced by:  orc  866  olc  867  pm2.68  899  pm4.79  1004  19.30  1880  axi12  2709  r19.30  3126  r19.30OLD  3127  sspss  4125  eqoreldif  4708  pwpw0  4838  sssn  4851  unissint  4996  disjiund  5157  disjxiun  5163  otsndisj  5538  otiunsndisj  5539  pwssun  5590  isso2i  5644  ordtr3  6440  ordtri2or  6493  unizlim  6518  fvclss  7278  orduniorsuc  7866  ordzsl  7882  nn0suc  7934  xpexr  7958  soseq  8200  odi  8635  swoso  8797  erdisj  8817  ordtypelem7  9593  wemapsolem  9619  domwdom  9643  iscard3  10162  ackbij1lem18  10305  fin56  10462  entric  10626  gchdomtri  10698  inttsk  10843  r1tskina  10851  psslinpr  11100  ssxr  11359  letric  11390  mul0or  11930  mulge0b  12165  zeo  12729  uzm1  12941  xrletri  13215  supxrgtmnf  13391  sq01  14274  ruclem3  16281  prm2orodd  16738  phiprmpw  16823  pleval2i  18406  irredn0  20449  drngmul0orOLD  20783  lvecvs0or  21133  lssvs0or  21135  lspsnat  21170  lsppratlem1  21172  domnchr  21570  fctop  23032  cctop  23034  ppttop  23035  clslp  23177  restntr  23211  cnconn  23451  txindis  23663  txconn  23718  isufil2  23937  ufprim  23938  alexsubALTlem3  24078  pmltpc  25504  iundisj2  25603  limcco  25948  fta1b  26231  aalioulem2  26393  abelthlem2  26494  logreclem  26823  dchrfi  27317  2sqb  27494  nosepdmlem  27746  noetasuplem4  27799  sletric  27827  muls0ord  28229  tgbtwnconn1  28601  legov3  28624  coltr  28673  colline  28675  tglowdim2ln  28677  ragflat3  28732  ragperp  28743  lmieu  28810  lmicom  28814  lmimid  28820  numedglnl  29179  nvmul0or  30682  hvmul0or  31057  atomli  32414  atordi  32416  iundisj2f  32612  iundisj2fi  32802  chnind  32983  mxidlprm  33463  ssmxidl  33467  qsdrng  33490  zarclssn  33819  signsply0  34528  pthisspthorcycl  35096  cvmsdisj  35238  nepss  35680  dfon2lem6  35752  btwnconn1lem13  36063  wl-exeq  37488  eqvreldisj  38570  lsator0sp  38957  lkreqN  39126  2at0mat0  39482  trlator0  40128  dochkrshp4  41346  dochsat0  41414  lcfl6  41457  expeqidd  42312  rp-fakeimass  43474  frege124d  43723  clsk1independent  44008  mnringmulrcld  44197  pm10.57  44340  icccncfext  45808  fourierdlem70  46097  ichnreuop  47346  uzlidlring  47958  nneop  48260  mo0sn  48547