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  4660  disji2  5103  disjxiun  5116  pwssun  5545  swopo  5572  sotric  5591  sotrieq  5592  somo  5600  ordtri3or  6384  ordtri1  6385  suc11  6460  foconst  6804  ordeleqon  7774  ssonprc  7779  onmindif2  7799  limsssuc  7843  limom  7875  onfununi  8353  oeeulem  8611  uniinqs  8809  pw2f1olem  9088  pssnn  9180  ordtypelem9  9538  ordtypelem10  9539  oismo  9552  preleqALT  9629  suc11reg  9631  cantnfp1lem2  9691  cantnflem1  9701  cnfcom2lem  9713  cnfcom3lem  9715  rankxpsuc  9894  cardlim  9984  alephdom  10093  cardaleph  10101  iscard3  10105  pwdjudom  10227  cfslbn  10279  fin1a2lem12  10423  gchi  10636  tskssel  10769  inttsk  10786  inar1  10787  r1tskina  10794  tskuni  10795  gruina  10830  grur1  10832  nlt1pi  10918  nqereu  10941  leltne  11322  nneo  12675  zeo2  12678  xrleltne  13159  nltpnft  13178  ngtmnft  13180  xrrebnd  13182  xaddf  13238  xrsupsslem  13321  xrinfmsslem  13322  fzocatel  13743  seqf1olem1  14057  seqf1olem2  14058  znsqcld  14178  discr1  14255  hashnncl  14382  seqcoll2  14481  sqeqd  15183  sqrmo  15268  isercoll  15682  bitsfzo  16452  bitsinv1lem  16458  bitsf1  16463  bezoutlem3  16558  eucalglt  16602  phibndlem  16787  dfphi2  16791  prmdiv  16802  odzdvds  16813  pceq0  16889  pc2dvds  16897  fldivp1  16915  pcfac  16917  prmreclem3  16936  1arith  16945  4sqlem10  16965  4sqlem17  16979  4sqlem18  16980  vdwlem6  17004  ramubcl  17036  ramcl  17047  mrissmrcd  17650  psgnunilem5  19473  oddvdsnn0  19523  odnncl  19524  oddvds  19526  odcl2  19544  gexdvds  19563  gexnnod  19567  sylow1lem1  19577  odcau  19583  pgpssslw  19593  efgs1b  19715  efgredlema  19719  torsubg  19833  prmcyg  19873  gsumval3eu  19883  ablfacrplem  20046  ablfac1eu  20054  ablsimpgprmd  20096  fidomndrnglem  20730  lspdisj  21084  lspsncv0  21105  gzrngunitlem  21398  prmirredlem  21431  fctop  22940  cctop  22942  ppttop  22943  pptbas  22944  ordtrest2lem  23139  connclo  23351  txindis  23570  filconn  23819  ufilb  23842  cldsubg  24047  reconnlem1  24764  reconnlem2  24765  metds0  24788  metdseq0  24792  metnrmlem1a  24796  iccpnfhmeo  24892  xrhmeo  24893  cphsubrglem  25127  minveclem3b  25378  minveclem4a  25380  vitalilem4  25562  itg2gt0  25711  itgsplitioo  25789  limccnp2  25843  rollelem  25943  dvlip  25948  itgsubstlem  26005  plyaddlem1  26168  plymullem1  26169  coefv0  26203  dgreq0  26221  radcnv0  26375  pserdvlem2  26388  pilem2  26412  sineq0  26483  logtayl  26619  cxpsqrt  26662  isosctrlem2  26779  atantayl2  26898  rlimcnp2  26926  amgm  26951  basellem3  27043  muval2  27094  sqf11  27099  ppinprm  27112  chtnprm  27114  perfectlem2  27191  lgsdir  27293  lgsabs1  27297  lgseisenlem1  27336  2sqlem7  27385  2sqblem  27392  2sqmod  27397  2sqreultblem  27409  2sqreunnltblem  27412  chebbnd1lem1  27430  dchrisum0flblem1  27469  pntpbnd1  27547  pntpbnd2  27548  ostth  27600  nosepon  27627  abssge0  28186  elnns2  28261  dfnns2  28279  symquadlem  28614  midexlem  28617  colperp  28654  midex  28662  oppperpex  28678  hlpasch  28681  hpgerlem  28690  colopp  28694  lmieu  28709  lmicom  28713  trgcopy  28729  cgracol  28753  minvecolem5  30808  staddi  32173  stadd3i  32175  atsseq  32274  atom1d  32280  atoml2i  32310  disji2f  32504  disjif2  32508  fprodex01  32750  sgn3da  32759  psgnfzto1stlem  33057  lvecdim0  33592  ordtrest2NEWlem  33899  eulerpartlemb  34346  subfacp1lem6  35153  cvmscld  35241  cvmsss2  35242  cvmseu  35244  ordtoplem  36399  ordcmp  36411  poimirlem25  37615  heiborlem6  37786  isfldidl  38038  pridlc2  38042  mpobi123f  38132  mptbi12f  38136  ac6s6  38142  lsatcmp  38967  lsatcmp2  38968  2atm  39492  trlatn0  40137  trlval3  40152  cdleme18c  40258  cdlemg17b  40627  cdlemg17i  40634  cdlemh  40782  dia2dimlem2  41030  dia2dimlem3  41031  dochlkr  41350  dochkrshp  41351  lcfl6  41465  lcfrlem9  41515  hdmap14lem6  41838  hgmapval0  41857  ioin9i8  42204  ctbnfien  42788  pw2f1ocnv  43008  unxpwdom3  43066  dgrsub2  43106  dflim5  43300  rp-fakeanorass  43484  mnuprdlem1  44244  mnuprdlem2  44245  mnurndlem1  44253  disjxp1  45041  fmul01lt1lem1  45561  elprn1  45610  stoweidlem35  46012  stirlinglem5  46055  stirlinglem12  46062  fourierdlem42  46126  fourierdlem93  46176  perfectALTVlem2  47684