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  4636  disji2  5076  disjxiun  5089  pwssun  5511  swopo  5538  sotric  5557  sotrieq  5558  somo  5566  ordtri3or  6339  ordtri1  6340  suc11  6416  foconst  6751  ordeleqon  7718  ssonprc  7723  onmindif2  7743  limsssuc  7783  limom  7815  onfununi  8264  oeeulem  8519  uniinqs  8724  pw2f1olem  8998  pssnn  9082  ordtypelem9  9418  ordtypelem10  9419  oismo  9432  preleqALT  9513  suc11reg  9515  cantnfp1lem2  9575  cantnflem1  9585  cnfcom2lem  9597  cnfcom3lem  9599  rankxpsuc  9778  cardlim  9868  alephdom  9975  cardaleph  9983  iscard3  9987  pwdjudom  10109  cfslbn  10161  fin1a2lem12  10305  gchi  10518  tskssel  10651  inttsk  10668  inar1  10669  r1tskina  10676  tskuni  10677  gruina  10712  grur1  10714  nlt1pi  10800  nqereu  10823  leltne  11205  nneo  12560  zeo2  12563  xrleltne  13047  nltpnft  13066  ngtmnft  13068  xrrebnd  13070  xaddf  13126  xrsupsslem  13209  xrinfmsslem  13210  fzocatel  13632  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  19373  oddvdsnn0  19423  odnncl  19424  oddvds  19426  odcl2  19444  gexdvds  19463  gexnnod  19467  sylow1lem1  19477  odcau  19483  pgpssslw  19493  efgs1b  19615  efgredlema  19619  torsubg  19733  prmcyg  19773  gsumval3eu  19783  ablfacrplem  19946  ablfac1eu  19954  ablsimpgprmd  19996  fidomndrnglem  20657  lspdisj  21032  lspsncv0  21053  gzrngunitlem  21339  prmirredlem  21379  fctop  22889  cctop  22891  ppttop  22892  pptbas  22893  ordtrest2lem  23088  connclo  23300  txindis  23519  filconn  23768  ufilb  23791  cldsubg  23996  reconnlem1  24713  reconnlem2  24714  metds0  24737  metdseq0  24741  metnrmlem1a  24745  iccpnfhmeo  24841  xrhmeo  24842  cphsubrglem  25075  minveclem3b  25326  minveclem4a  25328  vitalilem4  25510  itg2gt0  25659  itgsplitioo  25737  limccnp2  25791  rollelem  25891  dvlip  25896  itgsubstlem  25953  plyaddlem1  26116  plymullem1  26117  coefv0  26151  dgreq0  26169  radcnv0  26323  pserdvlem2  26336  pilem2  26360  sineq0  26431  logtayl  26567  cxpsqrt  26610  isosctrlem2  26727  atantayl2  26846  rlimcnp2  26874  amgm  26899  basellem3  26991  muval2  27042  sqf11  27047  ppinprm  27060  chtnprm  27062  perfectlem2  27139  lgsdir  27241  lgsabs1  27245  lgseisenlem1  27284  2sqlem7  27333  2sqblem  27340  2sqmod  27345  2sqreultblem  27357  2sqreunnltblem  27360  chebbnd1lem1  27378  dchrisum0flblem1  27417  pntpbnd1  27495  pntpbnd2  27496  ostth  27548  nosepon  27575  abssge0  28152  elnns2  28238  dfnns2  28266  symquadlem  28634  midexlem  28637  colperp  28674  midex  28682  oppperpex  28698  hlpasch  28701  hpgerlem  28710  colopp  28714  lmieu  28729  lmicom  28733  trgcopy  28749  cgracol  28773  minvecolem5  30825  staddi  32190  stadd3i  32192  atsseq  32291  atom1d  32297  atoml2i  32327  disji2f  32521  disjif2  32525  fprodex01  32771  sgn3da  32780  psgnfzto1stlem  33043  lvecdim0  33579  ordtrest2NEWlem  33895  eulerpartlemb  34342  subfacp1lem6  35168  cvmscld  35256  cvmsss2  35257  cvmseu  35259  ordtoplem  36419  ordcmp  36431  poimirlem25  37635  heiborlem6  37806  isfldidl  38058  pridlc2  38062  mpobi123f  38152  mptbi12f  38156  ac6s6  38162  lsatcmp  38992  lsatcmp2  38993  2atm  39516  trlatn0  40161  trlval3  40176  cdleme18c  40282  cdlemg17b  40651  cdlemg17i  40658  cdlemh  40806  dia2dimlem2  41054  dia2dimlem3  41055  dochlkr  41374  dochkrshp  41375  lcfl6  41489  lcfrlem9  41539  hdmap14lem6  41862  hgmapval0  41881  ioin9i8  42190  ctbnfien  42801  pw2f1ocnv  43020  unxpwdom3  43078  dgrsub2  43118  dflim5  43312  rp-fakeanorass  43496  mnuprdlem1  44255  mnuprdlem2  44256  mnurndlem1  44264  disjxp1  45057  fmul01lt1lem1  45575  elprn1  45624  stoweidlem35  46026  stirlinglem5  46069  stirlinglem12  46076  fourierdlem42  46140  fourierdlem93  46190  perfectALTVlem2  47716