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  4629  disji2  5070  disjxiun  5083  pwssun  5518  swopo  5545  sotric  5564  sotrieq  5565  somo  5573  ordtri3or  6351  ordtri1  6352  suc11  6428  foconst  6763  ordeleqon  7731  ssonprc  7736  onmindif2  7756  limsssuc  7796  limom  7828  onfununi  8276  oeeulem  8532  uniinqs  8739  pw2f1olem  9014  pssnn  9098  ordtypelem9  9436  ordtypelem10  9437  oismo  9450  preleqALT  9533  suc11reg  9535  cantnfp1lem2  9595  cantnflem1  9605  cnfcom2lem  9617  cnfcom3lem  9619  rankxpsuc  9801  cardlim  9891  alephdom  9998  cardaleph  10006  iscard3  10010  pwdjudom  10132  cfslbn  10184  fin1a2lem12  10328  gchi  10542  tskssel  10675  inttsk  10692  inar1  10693  r1tskina  10700  tskuni  10701  gruina  10736  grur1  10738  nlt1pi  10824  nqereu  10847  leltne  11230  nneo  12608  zeo2  12611  xrleltne  13091  nltpnft  13111  ngtmnft  13113  xrrebnd  13115  xaddf  13171  xrsupsslem  13254  xrinfmsslem  13255  fzocatel  13679  seqf1olem1  13998  seqf1olem2  13999  znsqcld  14119  discr1  14196  hashnncl  14323  seqcoll2  14422  sqeqd  15123  sqrmo  15208  isercoll  15625  bitsfzo  16399  bitsinv1lem  16405  bitsf1  16410  bezoutlem3  16505  eucalglt  16549  phibndlem  16735  dfphi2  16739  prmdiv  16750  odzdvds  16761  pceq0  16837  pc2dvds  16845  fldivp1  16863  pcfac  16865  prmreclem3  16884  1arith  16893  4sqlem10  16913  4sqlem17  16927  4sqlem18  16928  vdwlem6  16952  ramubcl  16984  ramcl  16995  mrissmrcd  17601  psgnunilem5  19464  oddvdsnn0  19514  odnncl  19515  oddvds  19517  odcl2  19535  gexdvds  19554  gexnnod  19558  sylow1lem1  19568  odcau  19574  pgpssslw  19584  efgs1b  19706  efgredlema  19710  torsubg  19824  prmcyg  19864  gsumval3eu  19874  ablfacrplem  20037  ablfac1eu  20045  ablsimpgprmd  20087  fidomndrnglem  20744  lspdisj  21119  lspsncv0  21140  gzrngunitlem  21426  prmirredlem  21466  fctop  22983  cctop  22985  ppttop  22986  pptbas  22987  ordtrest2lem  23182  connclo  23394  txindis  23613  filconn  23862  ufilb  23885  cldsubg  24090  reconnlem1  24806  reconnlem2  24807  metds0  24830  metdseq0  24834  metnrmlem1a  24838  iccpnfhmeo  24926  xrhmeo  24927  cphsubrglem  25158  minveclem3b  25409  minveclem4a  25411  vitalilem4  25592  itg2gt0  25741  itgsplitioo  25819  limccnp2  25873  rollelem  25970  dvlip  25974  itgsubstlem  26029  plyaddlem1  26192  plymullem1  26193  coefv0  26227  dgreq0  26244  radcnv0  26398  pserdvlem2  26410  pilem2  26434  sineq0  26505  logtayl  26641  cxpsqrt  26684  isosctrlem2  26800  atantayl2  26919  rlimcnp2  26947  amgm  26972  basellem3  27064  muval2  27115  sqf11  27120  ppinprm  27133  chtnprm  27135  perfectlem2  27211  lgsdir  27313  lgsabs1  27317  lgseisenlem1  27356  2sqlem7  27405  2sqblem  27412  2sqmod  27417  2sqreultblem  27429  2sqreunnltblem  27432  chebbnd1lem1  27450  dchrisum0flblem1  27489  pntpbnd1  27567  pntpbnd2  27568  ostth  27620  nosepon  27647  abssge0  28255  elnns2  28351  dfnns2  28382  z12bday  28495  symquadlem  28775  midexlem  28778  colperp  28815  midex  28823  oppperpex  28839  hlpasch  28842  hpgerlem  28851  colopp  28855  lmieu  28870  lmicom  28874  trgcopy  28890  cgracol  28914  minvecolem5  30971  staddi  32336  stadd3i  32338  atsseq  32437  atom1d  32443  atoml2i  32473  disji2f  32666  disjif2  32670  fprodex01  32917  sgn3da  32926  psgnfzto1stlem  33180  lvecdim0  33770  ordtrest2NEWlem  34086  eulerpartlemb  34532  subfacp1lem6  35387  cvmscld  35475  cvmsss2  35476  cvmseu  35478  ordtoplem  36637  ordcmp  36649  poimirlem25  37984  heiborlem6  38155  isfldidl  38407  pridlc2  38411  mpobi123f  38501  mptbi12f  38505  ac6s6  38511  lsatcmp  39467  lsatcmp2  39468  2atm  39991  trlatn0  40636  trlval3  40651  cdleme18c  40757  cdlemg17b  41126  cdlemg17i  41133  cdlemh  41281  dia2dimlem2  41529  dia2dimlem3  41530  dochlkr  41849  dochkrshp  41850  lcfl6  41964  lcfrlem9  42014  hdmap14lem6  42337  hgmapval0  42356  ioin9i8  42664  ctbnfien  43268  pw2f1ocnv  43487  unxpwdom3  43545  dgrsub2  43585  dflim5  43779  rp-fakeanorass  43962  mnuprdlem1  44721  mnuprdlem2  44722  mnurndlem1  44730  disjxp1  45522  fmul01lt1lem1  46036  stoweidlem35  46485  stirlinglem5  46528  stirlinglem12  46535  fourierdlem42  46599  fourierdlem93  46649  perfectALTVlem2  48214