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 221	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 210  df-or 848

This theorem is referenced by:  olcnd  877  orcanai  1003  ecase2d  1030  oplem1  1057  ornld  1062  ecase23d  1475  19.33b  1893  elpwunsn  4585  disji2  5021  disjxiun  5036  pwssun  5436  swopo  5464  sotric  5481  sotrieq  5482  somo  5490  ordtri3or  6223  ordtri1  6224  suc11  6294  foconst  6626  ordeleqon  7544  ssonprc  7549  onmindif2  7569  limsssuc  7607  limom  7638  onfununi  8056  oeeulem  8307  uniinqs  8457  pw2f1olem  8727  pssnn  8824  pssnnOLD  8872  ordtypelem9  9120  ordtypelem10  9121  oismo  9134  preleqALT  9210  suc11reg  9212  cantnfp1lem2  9272  cantnflem1  9282  cnfcom2lem  9294  cnfcom3lem  9296  rankxpsuc  9463  cardlim  9553  alephdom  9660  cardaleph  9668  iscard3  9672  pwdjudom  9795  cfslbn  9846  fin1a2lem12  9990  gchi  10203  tskssel  10336  inttsk  10353  inar1  10354  r1tskina  10361  tskuni  10362  gruina  10397  grur1  10399  nlt1pi  10485  nqereu  10508  leltne  10887  nneo  12226  zeo2  12229  xrleltne  12700  nltpnft  12719  ngtmnft  12721  xrrebnd  12723  xaddf  12779  xrsupsslem  12862  xrinfmsslem  12863  fzocatel  13271  seqf1olem1  13580  seqf1olem2  13581  znsqcld  13697  discr1  13771  hashnncl  13898  seqcoll2  13996  sqeqd  14694  sqrmo  14780  isercoll  15196  bitsfzo  15957  bitsinv1lem  15963  bitsf1  15968  bezoutlem3  16064  eucalglt  16105  phibndlem  16286  dfphi2  16290  prmdiv  16301  odzdvds  16311  pceq0  16387  pc2dvds  16395  fldivp1  16413  pcfac  16415  prmreclem3  16434  1arith  16443  4sqlem10  16463  4sqlem17  16477  4sqlem18  16478  vdwlem6  16502  ramubcl  16534  ramcl  16545  mrissmrcd  17097  psgnunilem5  18840  oddvdsnn0  18890  odnncl  18891  oddvds  18893  odcl2  18910  gexdvds  18927  gexnnod  18931  sylow1lem1  18941  odcau  18947  pgpssslw  18957  efgs1b  19080  efgredlema  19084  torsubg  19193  prmcyg  19233  gsumval3eu  19243  ablfacrplem  19406  ablfac1eu  19414  ablsimpgprmd  19456  lspdisj  20116  lspsncv0  20137  fidomndrnglem  20298  gzrngunitlem  20382  prmirredlem  20413  fctop  21855  cctop  21857  ppttop  21858  pptbas  21859  ordtrest2lem  22054  connclo  22266  txindis  22485  filconn  22734  ufilb  22757  cldsubg  22962  reconnlem1  23677  reconnlem2  23678  metds0  23701  metdseq0  23705  metnrmlem1a  23709  iccpnfhmeo  23796  xrhmeo  23797  cphsubrglem  24028  minveclem3b  24279  minveclem4a  24281  vitalilem4  24462  itg2gt0  24612  itgsplitioo  24689  limccnp2  24743  rollelem  24840  dvlip  24844  itgsubstlem  24899  plyaddlem1  25061  plymullem1  25062  coefv0  25096  dgreq0  25113  radcnv0  25262  pserdvlem2  25274  pilem2  25298  sineq0  25367  logtayl  25502  cxpsqrt  25545  isosctrlem2  25656  atantayl2  25775  rlimcnp2  25803  amgm  25827  basellem3  25919  muval2  25970  sqf11  25975  ppinprm  25988  chtnprm  25990  perfectlem2  26065  lgsdir  26167  lgsabs1  26171  lgseisenlem1  26210  2sqlem7  26259  2sqblem  26266  2sqmod  26271  2sqreultblem  26283  2sqreunnltblem  26286  chebbnd1lem1  26304  dchrisum0flblem1  26343  pntpbnd1  26421  pntpbnd2  26422  ostth  26474  symquadlem  26734  midexlem  26737  colperp  26774  midex  26782  oppperpex  26798  hlpasch  26801  hpgerlem  26810  colopp  26814  lmieu  26829  lmicom  26833  trgcopy  26849  cgracol  26873  minvecolem5  28916  staddi  30281  stadd3i  30283  atsseq  30382  atom1d  30388  atoml2i  30418  disji2f  30589  disjif2  30593  fprodex01  30813  psgnfzto1stlem  31040  lvecdim0  31358  ordtrest2NEWlem  31540  eulerpartlemb  32001  sgn3da  32174  subfacp1lem6  32814  cvmscld  32902  cvmsss2  32903  cvmseu  32905  nosepon  33554  ordtoplem  34310  ordcmp  34322  poimirlem25  35488  heiborlem6  35660  isfldidl  35912  pridlc2  35916  mpobi123f  36006  mptbi12f  36010  ac6s6  36016  lsatcmp  36703  lsatcmp2  36704  2atm  37227  trlatn0  37872  trlval3  37887  cdleme18c  37993  cdlemg17b  38362  cdlemg17i  38369  cdlemh  38517  dia2dimlem2  38765  dia2dimlem3  38766  dochlkr  39085  dochkrshp  39086  lcfl6  39200  lcfrlem9  39250  hdmap14lem6  39573  hgmapval0  39592  ioin9i8  39836  ctbnfien  40284  pw2f1ocnv  40503  unxpwdom3  40564  dgrsub2  40604  rp-fakeanorass  40746  mnuprdlem1  41504  mnuprdlem2  41505  mnurndlem1  41513  disjxp1  42231  fmul01lt1lem1  42743  elprn1  42792  stoweidlem35  43194  stirlinglem5  43237  stirlinglem12  43244  fourierdlem42  43308  fourierdlem93  43358  perfectALTVlem2  44790