Theorem ord 851

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

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

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 199  df-or 835

This theorem is referenced by:  orcanai  986  oplem1  1038  ornld  1043  ecase23d  1453  19.33b  1849  elpwunsn  4500  disji2  4918  disjxiun  4931  pwssun  5312  swopo  5340  sotric  5357  sotrieq  5358  somo  5366  ordtri3or  6066  ordtri1  6067  suc11  6137  foconst  6437  ordeleqon  7325  ssonprc  7329  onmindif2  7349  limsssuc  7387  limom  7417  onfununi  7788  oeeulem  8034  uniinqs  8183  pw2f1olem  8423  pssnn  8537  ordtypelem9  8791  ordtypelem10  8792  oismo  8805  preleqALT  8880  suc11reg  8882  cantnfp1lem2  8942  cantnflem1  8952  cnfcom2lem  8964  cnfcom3lem  8966  rankxpsuc  9111  cardlim  9201  alephdom  9307  cardaleph  9315  iscard3  9319  pwdjudom  9442  cfslbn  9493  fin1a2lem12  9637  gchi  9850  fpwwe2lem13  9868  tskssel  9983  inttsk  10000  inar1  10001  r1tskina  10008  tskuni  10009  gruina  10044  grur1  10046  nlt1pi  10132  nqereu  10155  leltne  10536  nneo  11885  zeo2  11888  xrleltne  12361  nltpnft  12380  ngtmnft  12382  xrrebnd  12384  xaddf  12440  xrsupsslem  12522  xrinfmsslem  12523  fzocatel  12922  seqf1olem1  13230  seqf1olem2  13231  znsqcld  13347  discr1  13421  hashnncl  13548  seqcoll2  13642  sqeqd  14392  sqrmo  14478  isercoll  14891  bitsfzo  15650  bitsinv1lem  15656  bitsf1  15661  bezoutlem3  15751  eucalglt  15791  phibndlem  15969  dfphi2  15973  prmdiv  15984  odzdvds  15994  pceq0  16069  pc2dvds  16077  fldivp1  16095  pcfac  16097  prmreclem3  16116  1arith  16125  4sqlem10  16145  4sqlem17  16159  4sqlem18  16160  vdwlem6  16184  ramubcl  16216  ramcl  16227  mrissmrcd  16781  psgnunilem5  18395  psgnunilem5OLD  18396  oddvdsnn0  18446  odnncl  18447  oddvds  18449  odcl2  18465  gexdvds  18482  gexnnod  18486  sylow1lem1  18496  odcau  18502  pgpssslw  18512  efgs1b  18632  efgredlema  18637  torsubg  18742  prmcyg  18780  gsumval3eu  18790  ablfacrplem  18949  ablfac1eu  18957  lspdisj  19631  lspsncv0  19652  fidomndrnglem  19812  gzrngunitlem  20327  prmirredlem  20357  fctop  21331  cctop  21333  ppttop  21334  pptbas  21335  ordtrest2lem  21530  connclo  21742  txindis  21961  filconn  22210  ufilb  22233  cldsubg  22437  reconnlem1  23152  reconnlem2  23153  metds0  23176  metdseq0  23180  metnrmlem1a  23184  iccpnfhmeo  23267  xrhmeo  23268  cphsubrglem  23499  minveclem3b  23749  minveclem4a  23751  vitalilem4  23930  itg2gt0  24079  itgsplitioo  24156  limccnp2  24208  rollelem  24304  dvlip  24308  itgsubstlem  24363  plyaddlem1  24521  plymullem1  24522  coefv0  24556  dgreq0  24573  radcnv0  24722  pserdvlem2  24734  pilem2  24758  sineq0  24827  logtayl  24959  cxpsqrt  25002  isosctrlem2  25113  atantayl2  25232  leibpilem1OLD  25235  rlimcnp2  25261  amgm  25285  basellem3  25377  muval2  25428  sqf11  25433  ppinprm  25446  chtnprm  25448  perfectlem2  25523  lgsdir  25625  lgsabs1  25629  lgseisenlem1  25668  2sqlem7  25717  2sqblem  25724  2sqmod  25729  2sqreultblem  25741  2sqreunnltblem  25744  chebbnd1lem1  25762  dchrisum0flblem1  25801  pntpbnd1  25879  pntpbnd2  25880  ostth  25932  symquadlem  26192  midexlem  26195  colperp  26232  midex  26240  oppperpex  26256  hlpasch  26259  hpgerlem  26268  colopp  26272  lmieu  26287  lmicom  26291  trgcopy  26307  cgracol  26331  minvecolem5  28451  staddi  29819  stadd3i  29821  atsseq  29920  atom1d  29926  atoml2i  29956  disji2f  30110  disjif2  30114  fprodex01  30311  lvecdim0  30666  psgnfzto1stlem  30723  ordtrest2NEWlem  30841  eulerpartlemb  31303  sgn3da  31477  subfacp1lem6  32057  cvmscld  32145  cvmsss2  32146  cvmseu  32148  nosepon  32733  ordtoplem  33343  ordcmp  33355  poimirlem25  34398  heiborlem6  34576  isfldidl  34828  pridlc2  34832  mpobi123f  34924  mptbi12f  34928  ac6s6  34934  lsatcmp  35624  lsatcmp2  35625  2atm  36148  trlatn0  36793  trlval3  36808  cdleme18c  36914  cdlemg17b  37283  cdlemg17i  37290  cdlemh  37438  dia2dimlem2  37686  dia2dimlem3  37687  dochlkr  38006  dochkrshp  38007  lcfl6  38121  lcfrlem9  38171  hdmap14lem6  38494  hgmapval0  38513  ioin9i8  38583  ctbnfien  38852  pw2f1ocnv  39071  unxpwdom3  39132  dgrsub2  39172  rp-fakeanorass  39316  mnuprdlem1  40024  mnuprdlem2  40025  mnurndlem1  40033  ablsimpgprmd  40091  disjxp1  40790  fmul01lt1lem1  41331  elprn1  41380  stoweidlem35  41786  stirlinglem5  41829  stirlinglem12  41836  fourierdlem42  41900  fourierdlem93  41950  perfectALTVlem2  43290