Theorem ord 875

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 859	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 220	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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

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 209  df-or 859

This theorem is referenced by:  olcnd  888  orcanai  1016  ecase2d  1043  oplem1  1068  ornld  1073  19.33b  1906  elpwunsn  4644  disji2  5085  disjxiun  5098  pwssun  5540  swopo  5567  sotric  5586  sotrieq  5587  somo  5595  ordtri3or  6379  ordtri1  6380  suc11  6456  foconst  6794  ordeleqon  7766  ssonprc  7771  onmindif2  7791  limsssuc  7831  limom  7863  onfununi  8313  oeeulem  8572  uniinqs  8780  pw2f1olem  9054  pssnn  9138  ordtypelem9  9475  ordtypelem10  9476  oismo  9489  preleqALT  9573  suc11reg  9575  cantnfp1lem2  9635  cantnflem1  9645  cnfcom2lem  9657  cnfcom3lem  9659  rankxpsuc  9841  cardlim  9931  alephdom  10038  cardaleph  10046  iscard3  10050  pwdjudom  10172  cfslbn  10225  fin1a2lem12  10369  gchi  10583  tskssel  10716  inttsk  10733  inar1  10734  r1tskina  10741  tskuni  10742  gruina  10777  grur1  10779  nlt1pi  10865  nqereu  10888  leltne  11273  nneo  12658  zeo2  12661  xrleltne  13148  nltpnft  13168  ngtmnft  13170  xrrebnd  13172  xaddf  13228  xrsupsslem  13311  xrinfmsslem  13312  fzocatel  13736  seqf1olem1  14055  seqf1olem2  14056  znsqcld  14176  discr1  14253  hashnncl  14380  seqcoll2  14479  sgn3da  15115  sqeqd  15194  sqrmo  15279  isercoll  15696  bitsfzo  16470  bitsinv1lem  16476  bitsf1  16481  bezoutlem3  16576  eucalglt  16620  phibndlem  16806  dfphi2  16810  prmdiv  16821  odzdvds  16832  pceq0  16908  pc2dvds  16916  fldivp1  16934  pcfac  16936  prmreclem3  16955  1arith  16964  4sqlem10  16984  4sqlem17  16998  4sqlem18  16999  vdwlem6  17023  ramubcl  17055  ramcl  17066  mrissmrcd  17673  psgnunilem5  19535  oddvdsnn0  19585  odnncl  19586  oddvds  19588  odcl2  19606  gexdvds  19625  gexnnod  19629  sylow1lem1  19639  odcau  19645  pgpssslw  19655  efgs1b  19777  efgredlema  19781  torsubg  19895  prmcyg  19935  gsumval3eu  19945  ablfacrplem  20108  ablfac1eu  20116  ablsimpgprmd  20158  fidomndrnglem  20823  lspdisj  21196  lspsncv0  21217  gzrngunitlem  21485  prmirredlem  21525  fctop  23065  cctop  23067  ppttop  23068  pptbas  23069  ordtrest2lem  23264  connclo  23476  txindis  23695  filconn  23944  ufilb  23967  cldsubg  24172  reconnlem1  24888  reconnlem2  24889  metds0  24912  metdseq0  24916  metnrmlem1a  24920  iccpnfhmeo  25008  xrhmeo  25009  cphsubrglem  25240  minveclem3b  25491  minveclem4a  25493  vitalilem4  25674  itg2gt0  25823  itgsplitioo  25901  limccnp2  25955  rollelem  26052  dvlip  26056  itgsubstlem  26111  plyaddlem1  26274  plymullem1  26275  coefv0  26309  dgreq0  26326  radcnv0  26480  pserdvlem2  26492  pilem2  26516  sineq0  26590  logtayl  26726  cxpsqrt  26769  isosctrlem2  26885  atantayl2  27004  rlimcnp2  27032  amgm  27056  basellem3  27148  muval2  27199  sqf11  27204  ppinprm  27217  chtnprm  27219  perfectlem2  27295  lgsdir  27397  lgsabs1  27401  lgseisenlem1  27440  2sqlem7  27489  2sqblem  27496  2sqmod  27501  2sqreultblem  27513  2sqreunnltblem  27516  chebbnd1lem1  27534  dchrisum0flblem1  27573  pntpbnd1  27651  pntpbnd2  27652  ostth  27704  nosepon  27730  abssge0  28339  elnns2  28435  dfnns2  28466  z12bday  28579  symquadlem  28863  midexlem  28866  colperp  28903  midex  28911  oppperpex  28927  hlpasch  28930  hpgerlem  28939  colopp  28943  lmieu  28958  lmicom  28962  trgcopy  28978  plngrotlem1  28995  cgracol  29023  minvecolem5  31085  staddi  32450  stadd3i  32452  atsseq  32551  atom1d  32557  atoml2i  32587  disji2f  32778  disjif2  32782  fprodex01  33028  psgnfzto1stlem  33281  lvecdim0  33905  ordtrest2NEWlem  34220  eulerpartlemb  34666  subfacp1lem6  35536  cvmscld  35624  cvmsss2  35625  cvmseu  35627  ordtoplem  36796  ordcmp  36808  poimirlem25  38145  heiborlem6  38316  isfldidl  38568  pridlc2  38572  mpobi123f  38662  mptbi12f  38666  ac6s6  38672  lsatcmp  39628  lsatcmp2  39629  2atm  40152  trlatn0  40797  trlval3  40812  cdleme18c  40918  cdlemg17b  41287  cdlemg17i  41294  cdlemh  41442  dia2dimlem2  41690  dia2dimlem3  41691  dochlkr  42010  dochkrshp  42011  lcfl6  42125  lcfrlem9  42175  hdmap14lem6  42498  hgmapval0  42517  ioin9i8  42825  ctbnfien  43396  pw2f1ocnv  43615  unxpwdom3  43673  dgrsub2  43713  dflim5  43907  rp-fakeanorass  44090  mnuprdlem1  44849  mnuprdlem2  44850  mnurndlem1  44858  disjxp1  45650  fmul01lt1lem1  46161  stoweidlem35  46610  stirlinglem5  46653  stirlinglem12  46660  fourierdlem42  46724  fourierdlem93  46774  perfectALTVlem2  48345