Theorem ord 862

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

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

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 206  df-or 846

This theorem is referenced by:  olcnd  875  orcanai  1001  ecase2d  1028  oplem1  1055  ornld  1060  ecase23d  1473  19.33b  1888  elpwunsn  4680  disji2  5123  disjxiun  5138  pwssun  5564  swopo  5592  sotric  5609  sotrieq  5610  somo  5618  ordtri3or  6385  ordtri1  6386  suc11  6460  foconst  6807  ordeleqon  7752  ssonprc  7758  onmindif2  7778  limsssuc  7822  limom  7854  onfununi  8323  oeeulem  8584  uniinqs  8774  pw2f1olem  9059  pssnn  9151  pssnnOLD  9248  ordtypelem9  9503  ordtypelem10  9504  oismo  9517  preleqALT  9594  suc11reg  9596  cantnfp1lem2  9656  cantnflem1  9666  cnfcom2lem  9678  cnfcom3lem  9680  rankxpsuc  9859  cardlim  9949  alephdom  10058  cardaleph  10066  iscard3  10070  pwdjudom  10193  cfslbn  10244  fin1a2lem12  10388  gchi  10601  tskssel  10734  inttsk  10751  inar1  10752  r1tskina  10759  tskuni  10760  gruina  10795  grur1  10797  nlt1pi  10883  nqereu  10906  leltne  11285  nneo  12628  zeo2  12631  xrleltne  13106  nltpnft  13125  ngtmnft  13127  xrrebnd  13129  xaddf  13185  xrsupsslem  13268  xrinfmsslem  13269  fzocatel  13678  seqf1olem1  13989  seqf1olem2  13990  znsqcld  14109  discr1  14184  hashnncl  14308  seqcoll2  14408  sqeqd  15095  sqrmo  15180  isercoll  15596  bitsfzo  16358  bitsinv1lem  16364  bitsf1  16369  bezoutlem3  16465  eucalglt  16504  phibndlem  16685  dfphi2  16689  prmdiv  16700  odzdvds  16710  pceq0  16786  pc2dvds  16794  fldivp1  16812  pcfac  16814  prmreclem3  16833  1arith  16842  4sqlem10  16862  4sqlem17  16876  4sqlem18  16877  vdwlem6  16901  ramubcl  16933  ramcl  16944  mrissmrcd  17566  psgnunilem5  19326  oddvdsnn0  19376  odnncl  19377  oddvds  19379  odcl2  19397  gexdvds  19416  gexnnod  19420  sylow1lem1  19430  odcau  19436  pgpssslw  19446  efgs1b  19568  efgredlema  19572  torsubg  19682  prmcyg  19721  gsumval3eu  19731  ablfacrplem  19894  ablfac1eu  19902  ablsimpgprmd  19944  lspdisj  20687  lspsncv0  20708  fidomndrnglem  20859  gzrngunitlem  20944  prmirredlem  20975  fctop  22436  cctop  22438  ppttop  22439  pptbas  22440  ordtrest2lem  22636  connclo  22848  txindis  23067  filconn  23316  ufilb  23339  cldsubg  23544  reconnlem1  24271  reconnlem2  24272  metds0  24295  metdseq0  24299  metnrmlem1a  24303  iccpnfhmeo  24390  xrhmeo  24391  cphsubrglem  24623  minveclem3b  24874  minveclem4a  24876  vitalilem4  25057  itg2gt0  25207  itgsplitioo  25284  limccnp2  25338  rollelem  25435  dvlip  25439  itgsubstlem  25494  plyaddlem1  25656  plymullem1  25657  coefv0  25691  dgreq0  25708  radcnv0  25857  pserdvlem2  25869  pilem2  25893  sineq0  25962  logtayl  26097  cxpsqrt  26140  isosctrlem2  26251  atantayl2  26370  rlimcnp2  26398  amgm  26422  basellem3  26514  muval2  26565  sqf11  26570  ppinprm  26583  chtnprm  26585  perfectlem2  26660  lgsdir  26762  lgsabs1  26766  lgseisenlem1  26805  2sqlem7  26854  2sqblem  26861  2sqmod  26866  2sqreultblem  26878  2sqreunnltblem  26881  chebbnd1lem1  26899  dchrisum0flblem1  26938  pntpbnd1  27016  pntpbnd2  27017  ostth  27069  nosepon  27095  symquadlem  27805  midexlem  27808  colperp  27845  midex  27853  oppperpex  27869  hlpasch  27872  hpgerlem  27881  colopp  27885  lmieu  27900  lmicom  27904  trgcopy  27920  cgracol  27944  minvecolem5  29997  staddi  31362  stadd3i  31364  atsseq  31463  atom1d  31469  atoml2i  31499  disji2f  31673  disjif2  31677  fprodex01  31902  psgnfzto1stlem  32130  lvecdim0  32530  ordtrest2NEWlem  32733  eulerpartlemb  33198  sgn3da  33371  subfacp1lem6  34007  cvmscld  34095  cvmsss2  34096  cvmseu  34098  ordtoplem  35124  ordcmp  35136  poimirlem25  36317  heiborlem6  36489  isfldidl  36741  pridlc2  36745  mpobi123f  36835  mptbi12f  36839  ac6s6  36845  lsatcmp  37678  lsatcmp2  37679  2atm  38203  trlatn0  38848  trlval3  38863  cdleme18c  38969  cdlemg17b  39338  cdlemg17i  39345  cdlemh  39493  dia2dimlem2  39741  dia2dimlem3  39742  dochlkr  40061  dochkrshp  40062  lcfl6  40176  lcfrlem9  40226  hdmap14lem6  40549  hgmapval0  40568  ioin9i8  40838  ctbnfien  41327  pw2f1ocnv  41547  unxpwdom3  41608  dgrsub2  41648  dflim5  41850  rp-fakeanorass  42035  mnuprdlem1  42802  mnuprdlem2  42803  mnurndlem1  42811  disjxp1  43527  fmul01lt1lem1  44073  elprn1  44122  stoweidlem35  44524  stirlinglem5  44567  stirlinglem12  44574  fourierdlem42  44638  fourierdlem93  44688  perfectALTVlem2  46162