Theorem ord 860

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

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

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 844

This theorem is referenced by:  olcnd  873  orcanai  999  ecase2d  1026  oplem1  1053  ornld  1058  ecase23d  1471  19.33b  1889  elpwunsn  4616  disji2  5052  disjxiun  5067  pwssun  5476  swopo  5505  sotric  5522  sotrieq  5523  somo  5531  ordtri3or  6283  ordtri1  6284  suc11  6354  foconst  6687  ordeleqon  7609  ssonprc  7614  onmindif2  7634  limsssuc  7672  limom  7703  onfununi  8143  oeeulem  8394  uniinqs  8544  pw2f1olem  8816  pssnn  8913  pssnnOLD  8969  ordtypelem9  9215  ordtypelem10  9216  oismo  9229  preleqALT  9305  suc11reg  9307  cantnfp1lem2  9367  cantnflem1  9377  cnfcom2lem  9389  cnfcom3lem  9391  rankxpsuc  9571  cardlim  9661  alephdom  9768  cardaleph  9776  iscard3  9780  pwdjudom  9903  cfslbn  9954  fin1a2lem12  10098  gchi  10311  tskssel  10444  inttsk  10461  inar1  10462  r1tskina  10469  tskuni  10470  gruina  10505  grur1  10507  nlt1pi  10593  nqereu  10616  leltne  10995  nneo  12334  zeo2  12337  xrleltne  12808  nltpnft  12827  ngtmnft  12829  xrrebnd  12831  xaddf  12887  xrsupsslem  12970  xrinfmsslem  12971  fzocatel  13379  seqf1olem1  13690  seqf1olem2  13691  znsqcld  13808  discr1  13882  hashnncl  14009  seqcoll2  14107  sqeqd  14805  sqrmo  14891  isercoll  15307  bitsfzo  16070  bitsinv1lem  16076  bitsf1  16081  bezoutlem3  16177  eucalglt  16218  phibndlem  16399  dfphi2  16403  prmdiv  16414  odzdvds  16424  pceq0  16500  pc2dvds  16508  fldivp1  16526  pcfac  16528  prmreclem3  16547  1arith  16556  4sqlem10  16576  4sqlem17  16590  4sqlem18  16591  vdwlem6  16615  ramubcl  16647  ramcl  16658  mrissmrcd  17266  psgnunilem5  19017  oddvdsnn0  19067  odnncl  19068  oddvds  19070  odcl2  19087  gexdvds  19104  gexnnod  19108  sylow1lem1  19118  odcau  19124  pgpssslw  19134  efgs1b  19257  efgredlema  19261  torsubg  19370  prmcyg  19410  gsumval3eu  19420  ablfacrplem  19583  ablfac1eu  19591  ablsimpgprmd  19633  lspdisj  20302  lspsncv0  20323  fidomndrnglem  20491  gzrngunitlem  20575  prmirredlem  20606  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  ordtrest2lem  22262  connclo  22474  txindis  22693  filconn  22942  ufilb  22965  cldsubg  23170  reconnlem1  23895  reconnlem2  23896  metds0  23919  metdseq0  23923  metnrmlem1a  23927  iccpnfhmeo  24014  xrhmeo  24015  cphsubrglem  24246  minveclem3b  24497  minveclem4a  24499  vitalilem4  24680  itg2gt0  24830  itgsplitioo  24907  limccnp2  24961  rollelem  25058  dvlip  25062  itgsubstlem  25117  plyaddlem1  25279  plymullem1  25280  coefv0  25314  dgreq0  25331  radcnv0  25480  pserdvlem2  25492  pilem2  25516  sineq0  25585  logtayl  25720  cxpsqrt  25763  isosctrlem2  25874  atantayl2  25993  rlimcnp2  26021  amgm  26045  basellem3  26137  muval2  26188  sqf11  26193  ppinprm  26206  chtnprm  26208  perfectlem2  26283  lgsdir  26385  lgsabs1  26389  lgseisenlem1  26428  2sqlem7  26477  2sqblem  26484  2sqmod  26489  2sqreultblem  26501  2sqreunnltblem  26504  chebbnd1lem1  26522  dchrisum0flblem1  26561  pntpbnd1  26639  pntpbnd2  26640  ostth  26692  symquadlem  26954  midexlem  26957  colperp  26994  midex  27002  oppperpex  27018  hlpasch  27021  hpgerlem  27030  colopp  27034  lmieu  27049  lmicom  27053  trgcopy  27069  cgracol  27093  minvecolem5  29144  staddi  30509  stadd3i  30511  atsseq  30610  atom1d  30616  atoml2i  30646  disji2f  30817  disjif2  30821  fprodex01  31041  psgnfzto1stlem  31269  lvecdim0  31592  ordtrest2NEWlem  31774  eulerpartlemb  32235  sgn3da  32408  subfacp1lem6  33047  cvmscld  33135  cvmsss2  33136  cvmseu  33138  nosepon  33795  ordtoplem  34551  ordcmp  34563  poimirlem25  35729  heiborlem6  35901  isfldidl  36153  pridlc2  36157  mpobi123f  36247  mptbi12f  36251  ac6s6  36257  lsatcmp  36944  lsatcmp2  36945  2atm  37468  trlatn0  38113  trlval3  38128  cdleme18c  38234  cdlemg17b  38603  cdlemg17i  38610  cdlemh  38758  dia2dimlem2  39006  dia2dimlem3  39007  dochlkr  39326  dochkrshp  39327  lcfl6  39441  lcfrlem9  39491  hdmap14lem6  39814  hgmapval0  39833  ioin9i8  40101  ctbnfien  40556  pw2f1ocnv  40775  unxpwdom3  40836  dgrsub2  40876  rp-fakeanorass  41018  mnuprdlem1  41779  mnuprdlem2  41780  mnurndlem1  41788  disjxp1  42506  fmul01lt1lem1  43015  elprn1  43064  stoweidlem35  43466  stirlinglem5  43509  stirlinglem12  43516  fourierdlem42  43580  fourierdlem93  43630  perfectALTVlem2  45062