Theorem ord 861

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

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

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 206  df-or 845

This theorem is referenced by:  olcnd  874  orcanai  1000  ecase2d  1027  oplem1  1054  ornld  1059  ecase23d  1472  19.33b  1889  elpwunsn  4620  disji2  5057  disjxiun  5072  pwssun  5486  swopo  5515  sotric  5532  sotrieq  5533  somo  5541  ordtri3or  6302  ordtri1  6303  suc11  6373  foconst  6712  ordeleqon  7641  ssonprc  7646  onmindif2  7666  limsssuc  7706  limom  7737  onfununi  8181  oeeulem  8441  uniinqs  8595  pw2f1olem  8872  pssnn  8960  pssnnOLD  9049  ordtypelem9  9294  ordtypelem10  9295  oismo  9308  preleqALT  9384  suc11reg  9386  cantnfp1lem2  9446  cantnflem1  9456  cnfcom2lem  9468  cnfcom3lem  9470  rankxpsuc  9649  cardlim  9739  alephdom  9846  cardaleph  9854  iscard3  9858  pwdjudom  9981  cfslbn  10032  fin1a2lem12  10176  gchi  10389  tskssel  10522  inttsk  10539  inar1  10540  r1tskina  10547  tskuni  10548  gruina  10583  grur1  10585  nlt1pi  10671  nqereu  10694  leltne  11073  nneo  12413  zeo2  12416  xrleltne  12888  nltpnft  12907  ngtmnft  12909  xrrebnd  12911  xaddf  12967  xrsupsslem  13050  xrinfmsslem  13051  fzocatel  13460  seqf1olem1  13771  seqf1olem2  13772  znsqcld  13889  discr1  13963  hashnncl  14090  seqcoll2  14188  sqeqd  14886  sqrmo  14972  isercoll  15388  bitsfzo  16151  bitsinv1lem  16157  bitsf1  16162  bezoutlem3  16258  eucalglt  16299  phibndlem  16480  dfphi2  16484  prmdiv  16495  odzdvds  16505  pceq0  16581  pc2dvds  16589  fldivp1  16607  pcfac  16609  prmreclem3  16628  1arith  16637  4sqlem10  16657  4sqlem17  16671  4sqlem18  16672  vdwlem6  16696  ramubcl  16728  ramcl  16739  mrissmrcd  17358  psgnunilem5  19111  oddvdsnn0  19161  odnncl  19162  oddvds  19164  odcl2  19181  gexdvds  19198  gexnnod  19202  sylow1lem1  19212  odcau  19218  pgpssslw  19228  efgs1b  19351  efgredlema  19355  torsubg  19464  prmcyg  19504  gsumval3eu  19514  ablfacrplem  19677  ablfac1eu  19685  ablsimpgprmd  19727  lspdisj  20396  lspsncv0  20417  fidomndrnglem  20587  gzrngunitlem  20672  prmirredlem  20703  fctop  22163  cctop  22165  ppttop  22166  pptbas  22167  ordtrest2lem  22363  connclo  22575  txindis  22794  filconn  23043  ufilb  23066  cldsubg  23271  reconnlem1  23998  reconnlem2  23999  metds0  24022  metdseq0  24026  metnrmlem1a  24030  iccpnfhmeo  24117  xrhmeo  24118  cphsubrglem  24350  minveclem3b  24601  minveclem4a  24603  vitalilem4  24784  itg2gt0  24934  itgsplitioo  25011  limccnp2  25065  rollelem  25162  dvlip  25166  itgsubstlem  25221  plyaddlem1  25383  plymullem1  25384  coefv0  25418  dgreq0  25435  radcnv0  25584  pserdvlem2  25596  pilem2  25620  sineq0  25689  logtayl  25824  cxpsqrt  25867  isosctrlem2  25978  atantayl2  26097  rlimcnp2  26125  amgm  26149  basellem3  26241  muval2  26292  sqf11  26297  ppinprm  26310  chtnprm  26312  perfectlem2  26387  lgsdir  26489  lgsabs1  26493  lgseisenlem1  26532  2sqlem7  26581  2sqblem  26588  2sqmod  26593  2sqreultblem  26605  2sqreunnltblem  26608  chebbnd1lem1  26626  dchrisum0flblem1  26665  pntpbnd1  26743  pntpbnd2  26744  ostth  26796  symquadlem  27059  midexlem  27062  colperp  27099  midex  27107  oppperpex  27123  hlpasch  27126  hpgerlem  27135  colopp  27139  lmieu  27154  lmicom  27158  trgcopy  27174  cgracol  27198  minvecolem5  29252  staddi  30617  stadd3i  30619  atsseq  30718  atom1d  30724  atoml2i  30754  disji2f  30925  disjif2  30929  fprodex01  31148  psgnfzto1stlem  31376  lvecdim0  31699  ordtrest2NEWlem  31881  eulerpartlemb  32344  sgn3da  32517  subfacp1lem6  33156  cvmscld  33244  cvmsss2  33245  cvmseu  33247  nosepon  33877  ordtoplem  34633  ordcmp  34645  poimirlem25  35811  heiborlem6  35983  isfldidl  36235  pridlc2  36239  mpobi123f  36329  mptbi12f  36333  ac6s6  36339  lsatcmp  37024  lsatcmp2  37025  2atm  37548  trlatn0  38193  trlval3  38208  cdleme18c  38314  cdlemg17b  38683  cdlemg17i  38690  cdlemh  38838  dia2dimlem2  39086  dia2dimlem3  39087  dochlkr  39406  dochkrshp  39407  lcfl6  39521  lcfrlem9  39571  hdmap14lem6  39894  hgmapval0  39913  ioin9i8  40180  ctbnfien  40647  pw2f1ocnv  40866  unxpwdom3  40927  dgrsub2  40967  rp-fakeanorass  41127  mnuprdlem1  41897  mnuprdlem2  41898  mnurndlem1  41906  disjxp1  42624  fmul01lt1lem1  43132  elprn1  43181  stoweidlem35  43583  stirlinglem5  43626  stirlinglem12  43633  fourierdlem42  43697  fourierdlem93  43747  perfectALTVlem2  45185