Theorem ord 865

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

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

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 849

This theorem is referenced by:  olcnd  878  orcanai  1005  ecase2d  1032  oplem1  1057  ornld  1062  ecase23d  1475  19.33b  1885  elpwunsn  4684  disji2  5127  disjxiun  5140  pwssun  5575  swopo  5603  sotric  5622  sotrieq  5623  somo  5631  ordtri3or  6416  ordtri1  6417  suc11  6491  foconst  6835  ordeleqon  7802  ssonprc  7807  onmindif2  7827  limsssuc  7871  limom  7903  onfununi  8381  oeeulem  8639  uniinqs  8837  pw2f1olem  9116  pssnn  9208  ordtypelem9  9566  ordtypelem10  9567  oismo  9580  preleqALT  9657  suc11reg  9659  cantnfp1lem2  9719  cantnflem1  9729  cnfcom2lem  9741  cnfcom3lem  9743  rankxpsuc  9922  cardlim  10012  alephdom  10121  cardaleph  10129  iscard3  10133  pwdjudom  10255  cfslbn  10307  fin1a2lem12  10451  gchi  10664  tskssel  10797  inttsk  10814  inar1  10815  r1tskina  10822  tskuni  10823  gruina  10858  grur1  10860  nlt1pi  10946  nqereu  10969  leltne  11350  nneo  12702  zeo2  12705  xrleltne  13187  nltpnft  13206  ngtmnft  13208  xrrebnd  13210  xaddf  13266  xrsupsslem  13349  xrinfmsslem  13350  fzocatel  13768  seqf1olem1  14082  seqf1olem2  14083  znsqcld  14202  discr1  14278  hashnncl  14405  seqcoll2  14504  sqeqd  15205  sqrmo  15290  isercoll  15704  bitsfzo  16472  bitsinv1lem  16478  bitsf1  16483  bezoutlem3  16578  eucalglt  16622  phibndlem  16807  dfphi2  16811  prmdiv  16822  odzdvds  16833  pceq0  16909  pc2dvds  16917  fldivp1  16935  pcfac  16937  prmreclem3  16956  1arith  16965  4sqlem10  16985  4sqlem17  16999  4sqlem18  17000  vdwlem6  17024  ramubcl  17056  ramcl  17067  mrissmrcd  17683  psgnunilem5  19512  oddvdsnn0  19562  odnncl  19563  oddvds  19565  odcl2  19583  gexdvds  19602  gexnnod  19606  sylow1lem1  19616  odcau  19622  pgpssslw  19632  efgs1b  19754  efgredlema  19758  torsubg  19872  prmcyg  19912  gsumval3eu  19922  ablfacrplem  20085  ablfac1eu  20093  ablsimpgprmd  20135  fidomndrnglem  20773  lspdisj  21127  lspsncv0  21148  gzrngunitlem  21450  prmirredlem  21483  fctop  23011  cctop  23013  ppttop  23014  pptbas  23015  ordtrest2lem  23211  connclo  23423  txindis  23642  filconn  23891  ufilb  23914  cldsubg  24119  reconnlem1  24848  reconnlem2  24849  metds0  24872  metdseq0  24876  metnrmlem1a  24880  iccpnfhmeo  24976  xrhmeo  24977  cphsubrglem  25211  minveclem3b  25462  minveclem4a  25464  vitalilem4  25646  itg2gt0  25795  itgsplitioo  25873  limccnp2  25927  rollelem  26027  dvlip  26032  itgsubstlem  26089  plyaddlem1  26252  plymullem1  26253  coefv0  26287  dgreq0  26305  radcnv0  26459  pserdvlem2  26472  pilem2  26496  sineq0  26566  logtayl  26702  cxpsqrt  26745  isosctrlem2  26862  atantayl2  26981  rlimcnp2  27009  amgm  27034  basellem3  27126  muval2  27177  sqf11  27182  ppinprm  27195  chtnprm  27197  perfectlem2  27274  lgsdir  27376  lgsabs1  27380  lgseisenlem1  27419  2sqlem7  27468  2sqblem  27475  2sqmod  27480  2sqreultblem  27492  2sqreunnltblem  27495  chebbnd1lem1  27513  dchrisum0flblem1  27552  pntpbnd1  27630  pntpbnd2  27631  ostth  27683  nosepon  27710  abssge0  28269  elnns2  28344  dfnns2  28362  symquadlem  28697  midexlem  28700  colperp  28737  midex  28745  oppperpex  28761  hlpasch  28764  hpgerlem  28773  colopp  28777  lmieu  28792  lmicom  28796  trgcopy  28812  cgracol  28836  minvecolem5  30900  staddi  32265  stadd3i  32267  atsseq  32366  atom1d  32372  atoml2i  32402  disji2f  32590  disjif2  32594  fprodex01  32827  psgnfzto1stlem  33120  lvecdim0  33657  ordtrest2NEWlem  33921  eulerpartlemb  34370  sgn3da  34544  subfacp1lem6  35190  cvmscld  35278  cvmsss2  35279  cvmseu  35281  ordtoplem  36436  ordcmp  36448  poimirlem25  37652  heiborlem6  37823  isfldidl  38075  pridlc2  38079  mpobi123f  38169  mptbi12f  38173  ac6s6  38179  lsatcmp  39004  lsatcmp2  39005  2atm  39529  trlatn0  40174  trlval3  40189  cdleme18c  40295  cdlemg17b  40664  cdlemg17i  40671  cdlemh  40819  dia2dimlem2  41067  dia2dimlem3  41068  dochlkr  41387  dochkrshp  41388  lcfl6  41502  lcfrlem9  41552  hdmap14lem6  41875  hgmapval0  41894  ioin9i8  42246  ctbnfien  42829  pw2f1ocnv  43049  unxpwdom3  43107  dgrsub2  43147  dflim5  43342  rp-fakeanorass  43526  mnuprdlem1  44291  mnuprdlem2  44292  mnurndlem1  44300  disjxp1  45074  fmul01lt1lem1  45599  elprn1  45648  stoweidlem35  46050  stirlinglem5  46093  stirlinglem12  46100  fourierdlem42  46164  fourierdlem93  46214  perfectALTVlem2  47709