Theorem ord 391

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

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

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 196  df-or 384

This theorem is referenced by:  ornld  938  orcanai  950  oplem1  999  ecase23d  1428  19.33b  1802  elpwunsn  4171  eqsnOLD  4302  disji2  4569  disjxiun  4579  disjxiunOLD  4580  pwssun  4944  swopo  4969  sotric  4985  sotrieq  4986  somo  4993  ordtri3or  5672  ordtri1  5673  ordtri3OLD  5677  suc11  5748  foconst  6039  ordeleqon  6880  ssonprc  6884  onmindif2  6904  limsssuc  6942  limom  6972  onfununi  7325  oeeulem  7568  uniinqs  7714  pw2f1olem  7949  pssnn  8063  ordtypelem9  8314  ordtypelem10  8315  oismo  8328  preleq  8397  suc11reg  8399  cantnfp1lem2  8459  cantnflem1  8469  cnfcom2lem  8481  cnfcom3lem  8483  rankxpsuc  8628  cardlim  8681  alephdom  8787  cardaleph  8795  iscard3  8799  pwcdadom  8921  cfslbn  8972  fin1a2lem12  9116  gchi  9325  fpwwe2lem13  9343  tskssel  9458  inttsk  9475  inar1  9476  r1tskina  9483  tskuni  9484  gruina  9519  grur1  9521  nlt1pi  9607  nqereu  9630  leltne  10006  nneo  11337  zeo2  11340  xrleltne  11854  nltpnft  11871  ngtmnft  11872  xrrebnd  11873  xaddf  11929  xrsupsslem  12009  xrinfmsslem  12010  fzocatel  12399  seqf1olem1  12702  seqf1olem2  12703  discr1  12862  hashnncl  13018  seqcoll2  13106  sqeqd  13754  sqrmo  13840  isercoll  14246  bitsfzo  14995  bitsinv1lem  15001  bitsf1  15006  bezoutlem3  15096  eucalglt  15136  phibndlem  15313  dfphi2  15317  prmdiv  15328  odzdvds  15338  pceq0  15413  pc2dvds  15421  fldivp1  15439  pcfac  15441  prmreclem3  15460  1arith  15469  4sqlem10  15489  4sqlem17  15503  4sqlem18  15504  vdwlem6  15528  ramubcl  15560  ramcl  15571  mrissmrcd  16123  psgnunilem5  17737  oddvdsnn0  17786  odnncl  17787  oddvds  17789  odcl2  17805  gexdvds  17822  gexnnod  17826  sylow1lem1  17836  odcau  17842  pgpssslw  17852  efgs1b  17972  efgredlema  17976  torsubg  18080  prmcyg  18118  gsumval3eu  18128  ablfacrplem  18287  ablfac1eu  18295  lspdisj  18946  lspsncv0  18967  fidomndrnglem  19127  gzrngunitlem  19630  prmirredlem  19660  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  ordtrest2lem  20817  conclo  21028  txindis  21247  filcon  21497  ufilb  21520  cldsubg  21724  reconnlem1  22437  reconnlem2  22438  metds0  22461  metdseq0  22465  metnrmlem1a  22469  iccpnfhmeo  22552  xrhmeo  22553  cphsubrglem  22785  minveclem3b  23007  minveclem4a  23009  vitalilem4  23186  itg2gt0  23333  itgsplitioo  23410  limccnp2  23462  rollelem  23556  dvlip  23560  itgsubstlem  23615  plyaddlem1  23773  plymullem1  23774  coefv0  23808  dgreq0  23825  radcnv0  23974  pserdvlem2  23986  pilem2  24010  sineq0  24077  logtayl  24206  cxpsqrt  24249  isosctrlem2  24349  atantayl2  24465  leibpilem1  24467  rlimcnp2  24493  amgm  24517  basellem3  24609  muval2  24660  sqf11  24665  ppinprm  24678  chtnprm  24680  perfectlem2  24755  lgsdir  24857  lgsabs1  24861  lgseisenlem1  24900  2sqlem7  24949  2sqblem  24956  chebbnd1lem1  24958  dchrisum0flblem1  24997  pntpbnd1  25075  pntpbnd2  25076  ostth  25128  symquadlem  25384  midexlem  25387  colperp  25421  midex  25429  oppperpex  25445  outpasch  25447  hlpasch  25448  hpgerlem  25457  colopp  25461  colhp  25462  lmieu  25476  lmicom  25480  trgcopy  25496  cgracol  25519  minvecolem5  27121  staddi  28489  stadd3i  28491  atsseq  28590  atom1d  28596  atoml2i  28626  disji2f  28772  disjif2  28776  znsqcld  28900  2sqmod  28979  psgnfzto1stlem  29181  ordtrest2NEWlem  29296  eulerpartlemb  29757  sgn3da  29930  subfacp1lem6  30421  cvmscld  30509  cvmsss2  30510  cvmseu  30512  nosepon  31066  ordtoplem  31604  ordcmp  31616  poimirlem25  32604  heiborlem6  32785  isfldidl  33037  pridlc2  33041  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  lsatcmp  33308  lsatcmp2  33309  2atm  33831  trlatn0  34477  trlval3  34492  cdleme18c  34598  cdlemg17b  34968  cdlemg17i  34975  cdlemh  35123  dia2dimlem2  35372  dia2dimlem3  35373  dochlkr  35692  dochkrshp  35693  lcfl6  35807  lcfrlem9  35857  hdmap14lem6  36183  hgmapval0  36202  ctbnfien  36400  pw2f1ocnv  36622  unxpwdom3  36683  dgrsub2  36724  rp-fakeanorass  36877  disjxp1  38263  fmul01lt1lem1  38651  elprn1  38700  stoweidlem35  38928  stirlinglem5  38971  stirlinglem12  38978  fourierdlem42  39042  fourierdlem93  39092  perfectALTVlem2  40165