Theorem ord 864

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
ord.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ord	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		df-or 848	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 218	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:  olcnd  877  orcanai  1004  ecase2d  1031  oplem1  1056  ornld  1061  19.33b  1885  elpwunsn  4651  disji2  5094  disjxiun  5107  pwssun  5533  swopo  5560  sotric  5579  sotrieq  5580  somo  5588  ordtri3or  6367  ordtri1  6368  suc11  6444  foconst  6790  ordeleqon  7761  ssonprc  7766  onmindif2  7786  limsssuc  7829  limom  7861  onfununi  8313  oeeulem  8568  uniinqs  8773  pw2f1olem  9050  pssnn  9138  ordtypelem9  9486  ordtypelem10  9487  oismo  9500  preleqALT  9577  suc11reg  9579  cantnfp1lem2  9639  cantnflem1  9649  cnfcom2lem  9661  cnfcom3lem  9663  rankxpsuc  9842  cardlim  9932  alephdom  10041  cardaleph  10049  iscard3  10053  pwdjudom  10175  cfslbn  10227  fin1a2lem12  10371  gchi  10584  tskssel  10717  inttsk  10734  inar1  10735  r1tskina  10742  tskuni  10743  gruina  10778  grur1  10780  nlt1pi  10866  nqereu  10889  leltne  11270  nneo  12625  zeo2  12628  xrleltne  13112  nltpnft  13131  ngtmnft  13133  xrrebnd  13135  xaddf  13191  xrsupsslem  13274  xrinfmsslem  13275  fzocatel  13697  seqf1olem1  14013  seqf1olem2  14014  znsqcld  14134  discr1  14211  hashnncl  14338  seqcoll2  14437  sqeqd  15139  sqrmo  15224  isercoll  15641  bitsfzo  16412  bitsinv1lem  16418  bitsf1  16423  bezoutlem3  16518  eucalglt  16562  phibndlem  16747  dfphi2  16751  prmdiv  16762  odzdvds  16773  pceq0  16849  pc2dvds  16857  fldivp1  16875  pcfac  16877  prmreclem3  16896  1arith  16905  4sqlem10  16925  4sqlem17  16939  4sqlem18  16940  vdwlem6  16964  ramubcl  16996  ramcl  17007  mrissmrcd  17608  psgnunilem5  19431  oddvdsnn0  19481  odnncl  19482  oddvds  19484  odcl2  19502  gexdvds  19521  gexnnod  19525  sylow1lem1  19535  odcau  19541  pgpssslw  19551  efgs1b  19673  efgredlema  19677  torsubg  19791  prmcyg  19831  gsumval3eu  19841  ablfacrplem  20004  ablfac1eu  20012  ablsimpgprmd  20054  fidomndrnglem  20688  lspdisj  21042  lspsncv0  21063  gzrngunitlem  21356  prmirredlem  21389  fctop  22898  cctop  22900  ppttop  22901  pptbas  22902  ordtrest2lem  23097  connclo  23309  txindis  23528  filconn  23777  ufilb  23800  cldsubg  24005  reconnlem1  24722  reconnlem2  24723  metds0  24746  metdseq0  24750  metnrmlem1a  24754  iccpnfhmeo  24850  xrhmeo  24851  cphsubrglem  25084  minveclem3b  25335  minveclem4a  25337  vitalilem4  25519  itg2gt0  25668  itgsplitioo  25746  limccnp2  25800  rollelem  25900  dvlip  25905  itgsubstlem  25962  plyaddlem1  26125  plymullem1  26126  coefv0  26160  dgreq0  26178  radcnv0  26332  pserdvlem2  26345  pilem2  26369  sineq0  26440  logtayl  26576  cxpsqrt  26619  isosctrlem2  26736  atantayl2  26855  rlimcnp2  26883  amgm  26908  basellem3  27000  muval2  27051  sqf11  27056  ppinprm  27069  chtnprm  27071  perfectlem2  27148  lgsdir  27250  lgsabs1  27254  lgseisenlem1  27293  2sqlem7  27342  2sqblem  27349  2sqmod  27354  2sqreultblem  27366  2sqreunnltblem  27369  chebbnd1lem1  27387  dchrisum0flblem1  27426  pntpbnd1  27504  pntpbnd2  27505  ostth  27557  nosepon  27584  abssge0  28154  elnns2  28240  dfnns2  28268  symquadlem  28623  midexlem  28626  colperp  28663  midex  28671  oppperpex  28687  hlpasch  28690  hpgerlem  28699  colopp  28703  lmieu  28718  lmicom  28722  trgcopy  28738  cgracol  28762  minvecolem5  30817  staddi  32182  stadd3i  32184  atsseq  32283  atom1d  32289  atoml2i  32319  disji2f  32513  disjif2  32517  fprodex01  32757  sgn3da  32766  psgnfzto1stlem  33064  lvecdim0  33609  ordtrest2NEWlem  33919  eulerpartlemb  34366  subfacp1lem6  35179  cvmscld  35267  cvmsss2  35268  cvmseu  35270  ordtoplem  36430  ordcmp  36442  poimirlem25  37646  heiborlem6  37817  isfldidl  38069  pridlc2  38073  mpobi123f  38163  mptbi12f  38167  ac6s6  38173  lsatcmp  39003  lsatcmp2  39004  2atm  39528  trlatn0  40173  trlval3  40188  cdleme18c  40294  cdlemg17b  40663  cdlemg17i  40670  cdlemh  40818  dia2dimlem2  41066  dia2dimlem3  41067  dochlkr  41386  dochkrshp  41387  lcfl6  41501  lcfrlem9  41551  hdmap14lem6  41874  hgmapval0  41893  ioin9i8  42202  ctbnfien  42813  pw2f1ocnv  43033  unxpwdom3  43091  dgrsub2  43131  dflim5  43325  rp-fakeanorass  43509  mnuprdlem1  44268  mnuprdlem2  44269  mnurndlem1  44277  disjxp1  45070  fmul01lt1lem1  45589  elprn1  45638  stoweidlem35  46040  stirlinglem5  46083  stirlinglem12  46090  fourierdlem42  46154  fourierdlem93  46204  perfectALTVlem2  47727