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  4648  disji2  5091  disjxiun  5104  pwssun  5530  swopo  5557  sotric  5576  sotrieq  5577  somo  5585  ordtri3or  6364  ordtri1  6365  suc11  6441  foconst  6787  ordeleqon  7758  ssonprc  7763  onmindif2  7783  limsssuc  7826  limom  7858  onfununi  8310  oeeulem  8565  uniinqs  8770  pw2f1olem  9045  pssnn  9132  ordtypelem9  9479  ordtypelem10  9480  oismo  9493  preleqALT  9570  suc11reg  9572  cantnfp1lem2  9632  cantnflem1  9642  cnfcom2lem  9654  cnfcom3lem  9656  rankxpsuc  9835  cardlim  9925  alephdom  10034  cardaleph  10042  iscard3  10046  pwdjudom  10168  cfslbn  10220  fin1a2lem12  10364  gchi  10577  tskssel  10710  inttsk  10727  inar1  10728  r1tskina  10735  tskuni  10736  gruina  10771  grur1  10773  nlt1pi  10859  nqereu  10882  leltne  11263  nneo  12618  zeo2  12621  xrleltne  13105  nltpnft  13124  ngtmnft  13126  xrrebnd  13128  xaddf  13184  xrsupsslem  13267  xrinfmsslem  13268  fzocatel  13690  seqf1olem1  14006  seqf1olem2  14007  znsqcld  14127  discr1  14204  hashnncl  14331  seqcoll2  14430  sqeqd  15132  sqrmo  15217  isercoll  15634  bitsfzo  16405  bitsinv1lem  16411  bitsf1  16416  bezoutlem3  16511  eucalglt  16555  phibndlem  16740  dfphi2  16744  prmdiv  16755  odzdvds  16766  pceq0  16842  pc2dvds  16850  fldivp1  16868  pcfac  16870  prmreclem3  16889  1arith  16898  4sqlem10  16918  4sqlem17  16932  4sqlem18  16933  vdwlem6  16957  ramubcl  16989  ramcl  17000  mrissmrcd  17601  psgnunilem5  19424  oddvdsnn0  19474  odnncl  19475  oddvds  19477  odcl2  19495  gexdvds  19514  gexnnod  19518  sylow1lem1  19528  odcau  19534  pgpssslw  19544  efgs1b  19666  efgredlema  19670  torsubg  19784  prmcyg  19824  gsumval3eu  19834  ablfacrplem  19997  ablfac1eu  20005  ablsimpgprmd  20047  fidomndrnglem  20681  lspdisj  21035  lspsncv0  21056  gzrngunitlem  21349  prmirredlem  21382  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  ordtrest2lem  23090  connclo  23302  txindis  23521  filconn  23770  ufilb  23793  cldsubg  23998  reconnlem1  24715  reconnlem2  24716  metds0  24739  metdseq0  24743  metnrmlem1a  24747  iccpnfhmeo  24843  xrhmeo  24844  cphsubrglem  25077  minveclem3b  25328  minveclem4a  25330  vitalilem4  25512  itg2gt0  25661  itgsplitioo  25739  limccnp2  25793  rollelem  25893  dvlip  25898  itgsubstlem  25955  plyaddlem1  26118  plymullem1  26119  coefv0  26153  dgreq0  26171  radcnv0  26325  pserdvlem2  26338  pilem2  26362  sineq0  26433  logtayl  26569  cxpsqrt  26612  isosctrlem2  26729  atantayl2  26848  rlimcnp2  26876  amgm  26901  basellem3  26993  muval2  27044  sqf11  27049  ppinprm  27062  chtnprm  27064  perfectlem2  27141  lgsdir  27243  lgsabs1  27247  lgseisenlem1  27286  2sqlem7  27335  2sqblem  27342  2sqmod  27347  2sqreultblem  27359  2sqreunnltblem  27362  chebbnd1lem1  27380  dchrisum0flblem1  27419  pntpbnd1  27497  pntpbnd2  27498  ostth  27550  nosepon  27577  abssge0  28147  elnns2  28233  dfnns2  28261  symquadlem  28616  midexlem  28619  colperp  28656  midex  28664  oppperpex  28680  hlpasch  28683  hpgerlem  28692  colopp  28696  lmieu  28711  lmicom  28715  trgcopy  28731  cgracol  28755  minvecolem5  30810  staddi  32175  stadd3i  32177  atsseq  32276  atom1d  32282  atoml2i  32312  disji2f  32506  disjif2  32510  fprodex01  32750  sgn3da  32759  psgnfzto1stlem  33057  lvecdim0  33602  ordtrest2NEWlem  33912  eulerpartlemb  34359  subfacp1lem6  35172  cvmscld  35260  cvmsss2  35261  cvmseu  35263  ordtoplem  36423  ordcmp  36435  poimirlem25  37639  heiborlem6  37810  isfldidl  38062  pridlc2  38066  mpobi123f  38156  mptbi12f  38160  ac6s6  38166  lsatcmp  38996  lsatcmp2  38997  2atm  39521  trlatn0  40166  trlval3  40181  cdleme18c  40287  cdlemg17b  40656  cdlemg17i  40663  cdlemh  40811  dia2dimlem2  41059  dia2dimlem3  41060  dochlkr  41379  dochkrshp  41380  lcfl6  41494  lcfrlem9  41544  hdmap14lem6  41867  hgmapval0  41886  ioin9i8  42195  ctbnfien  42806  pw2f1ocnv  43026  unxpwdom3  43084  dgrsub2  43124  dflim5  43318  rp-fakeanorass  43502  mnuprdlem1  44261  mnuprdlem2  44262  mnurndlem1  44270  disjxp1  45063  fmul01lt1lem1  45582  elprn1  45631  stoweidlem35  46033  stirlinglem5  46076  stirlinglem12  46083  fourierdlem42  46147  fourierdlem93  46197  perfectALTVlem2  47723