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  4644  disji2  5086  disjxiun  5099  pwssun  5523  swopo  5550  sotric  5569  sotrieq  5570  somo  5578  ordtri3or  6352  ordtri1  6353  suc11  6429  foconst  6769  ordeleqon  7738  ssonprc  7743  onmindif2  7763  limsssuc  7806  limom  7838  onfununi  8287  oeeulem  8542  uniinqs  8747  pw2f1olem  9022  pssnn  9109  ordtypelem9  9455  ordtypelem10  9456  oismo  9469  preleqALT  9546  suc11reg  9548  cantnfp1lem2  9608  cantnflem1  9618  cnfcom2lem  9630  cnfcom3lem  9632  rankxpsuc  9811  cardlim  9901  alephdom  10010  cardaleph  10018  iscard3  10022  pwdjudom  10144  cfslbn  10196  fin1a2lem12  10340  gchi  10553  tskssel  10686  inttsk  10703  inar1  10704  r1tskina  10711  tskuni  10712  gruina  10747  grur1  10749  nlt1pi  10835  nqereu  10858  leltne  11239  nneo  12594  zeo2  12597  xrleltne  13081  nltpnft  13100  ngtmnft  13102  xrrebnd  13104  xaddf  13160  xrsupsslem  13243  xrinfmsslem  13244  fzocatel  13666  seqf1olem1  13982  seqf1olem2  13983  znsqcld  14103  discr1  14180  hashnncl  14307  seqcoll2  14406  sqeqd  15108  sqrmo  15193  isercoll  15610  bitsfzo  16381  bitsinv1lem  16387  bitsf1  16392  bezoutlem3  16487  eucalglt  16531  phibndlem  16716  dfphi2  16720  prmdiv  16731  odzdvds  16742  pceq0  16818  pc2dvds  16826  fldivp1  16844  pcfac  16846  prmreclem3  16865  1arith  16874  4sqlem10  16894  4sqlem17  16908  4sqlem18  16909  vdwlem6  16933  ramubcl  16965  ramcl  16976  mrissmrcd  17581  psgnunilem5  19408  oddvdsnn0  19458  odnncl  19459  oddvds  19461  odcl2  19479  gexdvds  19498  gexnnod  19502  sylow1lem1  19512  odcau  19518  pgpssslw  19528  efgs1b  19650  efgredlema  19654  torsubg  19768  prmcyg  19808  gsumval3eu  19818  ablfacrplem  19981  ablfac1eu  19989  ablsimpgprmd  20031  fidomndrnglem  20692  lspdisj  21067  lspsncv0  21088  gzrngunitlem  21374  prmirredlem  21414  fctop  22924  cctop  22926  ppttop  22927  pptbas  22928  ordtrest2lem  23123  connclo  23335  txindis  23554  filconn  23803  ufilb  23826  cldsubg  24031  reconnlem1  24748  reconnlem2  24749  metds0  24772  metdseq0  24776  metnrmlem1a  24780  iccpnfhmeo  24876  xrhmeo  24877  cphsubrglem  25110  minveclem3b  25361  minveclem4a  25363  vitalilem4  25545  itg2gt0  25694  itgsplitioo  25772  limccnp2  25826  rollelem  25926  dvlip  25931  itgsubstlem  25988  plyaddlem1  26151  plymullem1  26152  coefv0  26186  dgreq0  26204  radcnv0  26358  pserdvlem2  26371  pilem2  26395  sineq0  26466  logtayl  26602  cxpsqrt  26645  isosctrlem2  26762  atantayl2  26881  rlimcnp2  26909  amgm  26934  basellem3  27026  muval2  27077  sqf11  27082  ppinprm  27095  chtnprm  27097  perfectlem2  27174  lgsdir  27276  lgsabs1  27280  lgseisenlem1  27319  2sqlem7  27368  2sqblem  27375  2sqmod  27380  2sqreultblem  27392  2sqreunnltblem  27395  chebbnd1lem1  27413  dchrisum0flblem1  27452  pntpbnd1  27530  pntpbnd2  27531  ostth  27583  nosepon  27610  abssge0  28187  elnns2  28273  dfnns2  28301  symquadlem  28669  midexlem  28672  colperp  28709  midex  28717  oppperpex  28733  hlpasch  28736  hpgerlem  28745  colopp  28749  lmieu  28764  lmicom  28768  trgcopy  28784  cgracol  28808  minvecolem5  30860  staddi  32225  stadd3i  32227  atsseq  32326  atom1d  32332  atoml2i  32362  disji2f  32556  disjif2  32560  fprodex01  32800  sgn3da  32809  psgnfzto1stlem  33072  lvecdim0  33595  ordtrest2NEWlem  33905  eulerpartlemb  34352  subfacp1lem6  35165  cvmscld  35253  cvmsss2  35254  cvmseu  35256  ordtoplem  36416  ordcmp  36428  poimirlem25  37632  heiborlem6  37803  isfldidl  38055  pridlc2  38059  mpobi123f  38149  mptbi12f  38153  ac6s6  38159  lsatcmp  38989  lsatcmp2  38990  2atm  39514  trlatn0  40159  trlval3  40174  cdleme18c  40280  cdlemg17b  40649  cdlemg17i  40656  cdlemh  40804  dia2dimlem2  41052  dia2dimlem3  41053  dochlkr  41372  dochkrshp  41373  lcfl6  41487  lcfrlem9  41537  hdmap14lem6  41860  hgmapval0  41879  ioin9i8  42188  ctbnfien  42799  pw2f1ocnv  43019  unxpwdom3  43077  dgrsub2  43117  dflim5  43311  rp-fakeanorass  43495  mnuprdlem1  44254  mnuprdlem2  44255  mnurndlem1  44263  disjxp1  45056  fmul01lt1lem1  45575  elprn1  45624  stoweidlem35  46026  stirlinglem5  46069  stirlinglem12  46076  fourierdlem42  46140  fourierdlem93  46190  perfectALTVlem2  47716