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  19.33b  1887  elpwunsn  4642  disji2  5083  disjxiun  5096  pwssun  5517  swopo  5544  sotric  5563  sotrieq  5564  somo  5572  ordtri3or  6350  ordtri1  6351  suc11  6427  foconst  6762  ordeleqon  7729  ssonprc  7734  onmindif2  7754  limsssuc  7794  limom  7826  onfununi  8275  oeeulem  8531  uniinqs  8738  pw2f1olem  9013  pssnn  9097  ordtypelem9  9435  ordtypelem10  9436  oismo  9449  preleqALT  9530  suc11reg  9532  cantnfp1lem2  9592  cantnflem1  9602  cnfcom2lem  9614  cnfcom3lem  9616  rankxpsuc  9798  cardlim  9888  alephdom  9995  cardaleph  10003  iscard3  10007  pwdjudom  10129  cfslbn  10181  fin1a2lem12  10325  gchi  10539  tskssel  10672  inttsk  10689  inar1  10690  r1tskina  10697  tskuni  10698  gruina  10733  grur1  10735  nlt1pi  10821  nqereu  10844  leltne  11226  nneo  12580  zeo2  12583  xrleltne  13063  nltpnft  13083  ngtmnft  13085  xrrebnd  13087  xaddf  13143  xrsupsslem  13226  xrinfmsslem  13227  fzocatel  13649  seqf1olem1  13968  seqf1olem2  13969  znsqcld  14089  discr1  14166  hashnncl  14293  seqcoll2  14392  sqeqd  15093  sqrmo  15178  isercoll  15595  bitsfzo  16366  bitsinv1lem  16372  bitsf1  16377  bezoutlem3  16472  eucalglt  16516  phibndlem  16701  dfphi2  16705  prmdiv  16716  odzdvds  16727  pceq0  16803  pc2dvds  16811  fldivp1  16829  pcfac  16831  prmreclem3  16850  1arith  16859  4sqlem10  16879  4sqlem17  16893  4sqlem18  16894  vdwlem6  16918  ramubcl  16950  ramcl  16961  mrissmrcd  17567  psgnunilem5  19427  oddvdsnn0  19477  odnncl  19478  oddvds  19480  odcl2  19498  gexdvds  19517  gexnnod  19521  sylow1lem1  19531  odcau  19537  pgpssslw  19547  efgs1b  19669  efgredlema  19673  torsubg  19787  prmcyg  19827  gsumval3eu  19837  ablfacrplem  20000  ablfac1eu  20008  ablsimpgprmd  20050  fidomndrnglem  20709  lspdisj  21084  lspsncv0  21105  gzrngunitlem  21391  prmirredlem  21431  fctop  22952  cctop  22954  ppttop  22955  pptbas  22956  ordtrest2lem  23151  connclo  23363  txindis  23582  filconn  23831  ufilb  23854  cldsubg  24059  reconnlem1  24775  reconnlem2  24776  metds0  24799  metdseq0  24803  metnrmlem1a  24807  iccpnfhmeo  24903  xrhmeo  24904  cphsubrglem  25137  minveclem3b  25388  minveclem4a  25390  vitalilem4  25572  itg2gt0  25721  itgsplitioo  25799  limccnp2  25853  rollelem  25953  dvlip  25958  itgsubstlem  26015  plyaddlem1  26178  plymullem1  26179  coefv0  26213  dgreq0  26231  radcnv0  26385  pserdvlem2  26398  pilem2  26422  sineq0  26493  logtayl  26629  cxpsqrt  26672  isosctrlem2  26789  atantayl2  26908  rlimcnp2  26936  amgm  26961  basellem3  27053  muval2  27104  sqf11  27109  ppinprm  27122  chtnprm  27124  perfectlem2  27201  lgsdir  27303  lgsabs1  27307  lgseisenlem1  27346  2sqlem7  27395  2sqblem  27402  2sqmod  27407  2sqreultblem  27419  2sqreunnltblem  27422  chebbnd1lem1  27440  dchrisum0flblem1  27479  pntpbnd1  27557  pntpbnd2  27558  ostth  27610  nosepon  27637  abssge0  28245  elnns2  28341  dfnns2  28372  z12bday  28485  symquadlem  28765  midexlem  28768  colperp  28805  midex  28813  oppperpex  28829  hlpasch  28832  hpgerlem  28841  colopp  28845  lmieu  28860  lmicom  28864  trgcopy  28880  cgracol  28904  minvecolem5  30960  staddi  32325  stadd3i  32327  atsseq  32426  atom1d  32432  atoml2i  32462  disji2f  32655  disjif2  32659  fprodex01  32908  sgn3da  32917  psgnfzto1stlem  33184  lvecdim0  33765  ordtrest2NEWlem  34081  eulerpartlemb  34527  subfacp1lem6  35381  cvmscld  35469  cvmsss2  35470  cvmseu  35472  ordtoplem  36631  ordcmp  36643  poimirlem25  37848  heiborlem6  38019  isfldidl  38271  pridlc2  38275  mpobi123f  38365  mptbi12f  38369  ac6s6  38375  lsatcmp  39331  lsatcmp2  39332  2atm  39855  trlatn0  40500  trlval3  40515  cdleme18c  40621  cdlemg17b  40990  cdlemg17i  40997  cdlemh  41145  dia2dimlem2  41393  dia2dimlem3  41394  dochlkr  41713  dochkrshp  41714  lcfl6  41828  lcfrlem9  41878  hdmap14lem6  42201  hgmapval0  42220  ioin9i8  42529  ctbnfien  43127  pw2f1ocnv  43346  unxpwdom3  43404  dgrsub2  43444  dflim5  43638  rp-fakeanorass  43821  mnuprdlem1  44580  mnuprdlem2  44581  mnurndlem1  44589  disjxp1  45381  fmul01lt1lem1  45897  stoweidlem35  46346  stirlinglem5  46389  stirlinglem12  46396  fourierdlem42  46460  fourierdlem93  46510  perfectALTVlem2  48035