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 220	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 209  df-or 844

This theorem is referenced by:  olcnd  873  orcanai  999  oplem1  1051  ornld  1056  ecase23d  1469  19.33b  1886  elpwunsn  4621  disji2  5048  disjxiun  5063  pwssun  5456  swopo  5484  sotric  5501  sotrieq  5502  somo  5510  ordtri3or  6223  ordtri1  6224  suc11  6294  foconst  6603  ordeleqon  7503  ssonprc  7507  onmindif2  7527  limsssuc  7565  limom  7595  onfununi  7978  oeeulem  8227  uniinqs  8377  pw2f1olem  8621  pssnn  8736  ordtypelem9  8990  ordtypelem10  8991  oismo  9004  preleqALT  9080  suc11reg  9082  cantnfp1lem2  9142  cantnflem1  9152  cnfcom2lem  9164  cnfcom3lem  9166  rankxpsuc  9311  cardlim  9401  alephdom  9507  cardaleph  9515  iscard3  9519  pwdjudom  9638  cfslbn  9689  fin1a2lem12  9833  gchi  10046  fpwwe2lem13  10064  tskssel  10179  inttsk  10196  inar1  10197  r1tskina  10204  tskuni  10205  gruina  10240  grur1  10242  nlt1pi  10328  nqereu  10351  leltne  10730  nneo  12067  zeo2  12070  xrleltne  12539  nltpnft  12558  ngtmnft  12560  xrrebnd  12562  xaddf  12618  xrsupsslem  12701  xrinfmsslem  12702  fzocatel  13102  seqf1olem1  13410  seqf1olem2  13411  znsqcld  13527  discr1  13601  hashnncl  13728  seqcoll2  13824  sqeqd  14525  sqrmo  14611  isercoll  15024  bitsfzo  15784  bitsinv1lem  15790  bitsf1  15795  bezoutlem3  15889  eucalglt  15929  phibndlem  16107  dfphi2  16111  prmdiv  16122  odzdvds  16132  pceq0  16207  pc2dvds  16215  fldivp1  16233  pcfac  16235  prmreclem3  16254  1arith  16263  4sqlem10  16283  4sqlem17  16297  4sqlem18  16298  vdwlem6  16322  ramubcl  16354  ramcl  16365  mrissmrcd  16911  psgnunilem5  18622  oddvdsnn0  18672  odnncl  18673  oddvds  18675  odcl2  18692  gexdvds  18709  gexnnod  18713  sylow1lem1  18723  odcau  18729  pgpssslw  18739  efgs1b  18862  efgredlema  18866  torsubg  18974  prmcyg  19014  gsumval3eu  19024  ablfacrplem  19187  ablfac1eu  19195  ablsimpgprmd  19237  lspdisj  19897  lspsncv0  19918  fidomndrnglem  20079  gzrngunitlem  20610  prmirredlem  20640  fctop  21612  cctop  21614  ppttop  21615  pptbas  21616  ordtrest2lem  21811  connclo  22023  txindis  22242  filconn  22491  ufilb  22514  cldsubg  22719  reconnlem1  23434  reconnlem2  23435  metds0  23458  metdseq0  23462  metnrmlem1a  23466  iccpnfhmeo  23549  xrhmeo  23550  cphsubrglem  23781  minveclem3b  24031  minveclem4a  24033  vitalilem4  24212  itg2gt0  24361  itgsplitioo  24438  limccnp2  24490  rollelem  24586  dvlip  24590  itgsubstlem  24645  plyaddlem1  24803  plymullem1  24804  coefv0  24838  dgreq0  24855  radcnv0  25004  pserdvlem2  25016  pilem2  25040  sineq0  25109  logtayl  25243  cxpsqrt  25286  isosctrlem2  25397  atantayl2  25516  rlimcnp2  25544  amgm  25568  basellem3  25660  muval2  25711  sqf11  25716  ppinprm  25729  chtnprm  25731  perfectlem2  25806  lgsdir  25908  lgsabs1  25912  lgseisenlem1  25951  2sqlem7  26000  2sqblem  26007  2sqmod  26012  2sqreultblem  26024  2sqreunnltblem  26027  chebbnd1lem1  26045  dchrisum0flblem1  26084  pntpbnd1  26162  pntpbnd2  26163  ostth  26215  symquadlem  26475  midexlem  26478  colperp  26515  midex  26523  oppperpex  26539  hlpasch  26542  hpgerlem  26551  colopp  26555  lmieu  26570  lmicom  26574  trgcopy  26590  cgracol  26614  minvecolem5  28658  staddi  30023  stadd3i  30025  atsseq  30124  atom1d  30130  atoml2i  30160  disji2f  30327  disjif2  30331  fprodex01  30541  psgnfzto1stlem  30742  lvecdim0  31005  ordtrest2NEWlem  31165  eulerpartlemb  31626  sgn3da  31799  subfacp1lem6  32432  cvmscld  32520  cvmsss2  32521  cvmseu  32523  nosepon  33172  ordtoplem  33783  ordcmp  33795  poimirlem25  34932  heiborlem6  35109  isfldidl  35361  pridlc2  35365  mpobi123f  35455  mptbi12f  35459  ac6s6  35465  lsatcmp  36154  lsatcmp2  36155  2atm  36678  trlatn0  37323  trlval3  37338  cdleme18c  37444  cdlemg17b  37813  cdlemg17i  37820  cdlemh  37968  dia2dimlem2  38216  dia2dimlem3  38217  dochlkr  38536  dochkrshp  38537  lcfl6  38651  lcfrlem9  38701  hdmap14lem6  39024  hgmapval0  39043  ioin9i8  39119  ctbnfien  39435  pw2f1ocnv  39654  unxpwdom3  39715  dgrsub2  39755  rp-fakeanorass  39899  mnuprdlem1  40628  mnuprdlem2  40629  mnurndlem1  40637  disjxp1  41351  fmul01lt1lem1  41885  elprn1  41934  stoweidlem35  42340  stirlinglem5  42383  stirlinglem12  42390  fourierdlem42  42454  fourierdlem93  42504  perfectALTVlem2  43907