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  1886  elpwunsn  4634  disji2  5073  disjxiun  5086  pwssun  5506  swopo  5533  sotric  5552  sotrieq  5553  somo  5561  ordtri3or  6338  ordtri1  6339  suc11  6415  foconst  6750  ordeleqon  7715  ssonprc  7720  onmindif2  7740  limsssuc  7780  limom  7812  onfununi  8261  oeeulem  8516  uniinqs  8721  pw2f1olem  8994  pssnn  9078  ordtypelem9  9412  ordtypelem10  9413  oismo  9426  preleqALT  9507  suc11reg  9509  cantnfp1lem2  9569  cantnflem1  9579  cnfcom2lem  9591  cnfcom3lem  9593  rankxpsuc  9775  cardlim  9865  alephdom  9972  cardaleph  9980  iscard3  9984  pwdjudom  10106  cfslbn  10158  fin1a2lem12  10302  gchi  10515  tskssel  10648  inttsk  10665  inar1  10666  r1tskina  10673  tskuni  10674  gruina  10709  grur1  10711  nlt1pi  10797  nqereu  10820  leltne  11202  nneo  12557  zeo2  12560  xrleltne  13044  nltpnft  13063  ngtmnft  13065  xrrebnd  13067  xaddf  13123  xrsupsslem  13206  xrinfmsslem  13207  fzocatel  13629  seqf1olem1  13948  seqf1olem2  13949  znsqcld  14069  discr1  14146  hashnncl  14273  seqcoll2  14372  sqeqd  15073  sqrmo  15158  isercoll  15575  bitsfzo  16346  bitsinv1lem  16352  bitsf1  16357  bezoutlem3  16452  eucalglt  16496  phibndlem  16681  dfphi2  16685  prmdiv  16696  odzdvds  16707  pceq0  16783  pc2dvds  16791  fldivp1  16809  pcfac  16811  prmreclem3  16830  1arith  16839  4sqlem10  16859  4sqlem17  16873  4sqlem18  16874  vdwlem6  16898  ramubcl  16930  ramcl  16941  mrissmrcd  17546  psgnunilem5  19406  oddvdsnn0  19456  odnncl  19457  oddvds  19459  odcl2  19477  gexdvds  19496  gexnnod  19500  sylow1lem1  19510  odcau  19516  pgpssslw  19526  efgs1b  19648  efgredlema  19652  torsubg  19766  prmcyg  19806  gsumval3eu  19816  ablfacrplem  19979  ablfac1eu  19987  ablsimpgprmd  20029  fidomndrnglem  20687  lspdisj  21062  lspsncv0  21083  gzrngunitlem  21369  prmirredlem  21409  fctop  22919  cctop  22921  ppttop  22922  pptbas  22923  ordtrest2lem  23118  connclo  23330  txindis  23549  filconn  23798  ufilb  23821  cldsubg  24026  reconnlem1  24742  reconnlem2  24743  metds0  24766  metdseq0  24770  metnrmlem1a  24774  iccpnfhmeo  24870  xrhmeo  24871  cphsubrglem  25104  minveclem3b  25355  minveclem4a  25357  vitalilem4  25539  itg2gt0  25688  itgsplitioo  25766  limccnp2  25820  rollelem  25920  dvlip  25925  itgsubstlem  25982  plyaddlem1  26145  plymullem1  26146  coefv0  26180  dgreq0  26198  radcnv0  26352  pserdvlem2  26365  pilem2  26389  sineq0  26460  logtayl  26596  cxpsqrt  26639  isosctrlem2  26756  atantayl2  26875  rlimcnp2  26903  amgm  26928  basellem3  27020  muval2  27071  sqf11  27076  ppinprm  27089  chtnprm  27091  perfectlem2  27168  lgsdir  27270  lgsabs1  27274  lgseisenlem1  27313  2sqlem7  27362  2sqblem  27369  2sqmod  27374  2sqreultblem  27386  2sqreunnltblem  27389  chebbnd1lem1  27407  dchrisum0flblem1  27446  pntpbnd1  27524  pntpbnd2  27525  ostth  27577  nosepon  27604  abssge0  28183  elnns2  28269  dfnns2  28297  symquadlem  28667  midexlem  28670  colperp  28707  midex  28715  oppperpex  28731  hlpasch  28734  hpgerlem  28743  colopp  28747  lmieu  28762  lmicom  28766  trgcopy  28782  cgracol  28806  minvecolem5  30861  staddi  32226  stadd3i  32228  atsseq  32327  atom1d  32333  atoml2i  32363  disji2f  32557  disjif2  32561  fprodex01  32808  sgn3da  32817  psgnfzto1stlem  33069  lvecdim0  33619  ordtrest2NEWlem  33935  eulerpartlemb  34381  subfacp1lem6  35229  cvmscld  35317  cvmsss2  35318  cvmseu  35320  ordtoplem  36479  ordcmp  36491  poimirlem25  37695  heiborlem6  37866  isfldidl  38118  pridlc2  38122  mpobi123f  38212  mptbi12f  38216  ac6s6  38222  lsatcmp  39112  lsatcmp2  39113  2atm  39636  trlatn0  40281  trlval3  40296  cdleme18c  40402  cdlemg17b  40771  cdlemg17i  40778  cdlemh  40926  dia2dimlem2  41174  dia2dimlem3  41175  dochlkr  41494  dochkrshp  41495  lcfl6  41609  lcfrlem9  41659  hdmap14lem6  41982  hgmapval0  42001  ioin9i8  42310  ctbnfien  42921  pw2f1ocnv  43140  unxpwdom3  43198  dgrsub2  43238  dflim5  43432  rp-fakeanorass  43616  mnuprdlem1  44375  mnuprdlem2  44376  mnurndlem1  44384  disjxp1  45176  fmul01lt1lem1  45694  stoweidlem35  46143  stirlinglem5  46186  stirlinglem12  46193  fourierdlem42  46257  fourierdlem93  46307  perfectALTVlem2  47832