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  1886  elpwunsn  4639  disji2  5080  disjxiun  5093  pwssun  5514  swopo  5541  sotric  5560  sotrieq  5561  somo  5569  ordtri3or  6347  ordtri1  6348  suc11  6424  foconst  6759  ordeleqon  7725  ssonprc  7730  onmindif2  7750  limsssuc  7790  limom  7822  onfununi  8271  oeeulem  8527  uniinqs  8732  pw2f1olem  9007  pssnn  9091  ordtypelem9  9429  ordtypelem10  9430  oismo  9443  preleqALT  9524  suc11reg  9526  cantnfp1lem2  9586  cantnflem1  9596  cnfcom2lem  9608  cnfcom3lem  9610  rankxpsuc  9792  cardlim  9882  alephdom  9989  cardaleph  9997  iscard3  10001  pwdjudom  10123  cfslbn  10175  fin1a2lem12  10319  gchi  10533  tskssel  10666  inttsk  10683  inar1  10684  r1tskina  10691  tskuni  10692  gruina  10727  grur1  10729  nlt1pi  10815  nqereu  10838  leltne  11220  nneo  12574  zeo2  12577  xrleltne  13057  nltpnft  13077  ngtmnft  13079  xrrebnd  13081  xaddf  13137  xrsupsslem  13220  xrinfmsslem  13221  fzocatel  13643  seqf1olem1  13962  seqf1olem2  13963  znsqcld  14083  discr1  14160  hashnncl  14287  seqcoll2  14386  sqeqd  15087  sqrmo  15172  isercoll  15589  bitsfzo  16360  bitsinv1lem  16366  bitsf1  16371  bezoutlem3  16466  eucalglt  16510  phibndlem  16695  dfphi2  16699  prmdiv  16710  odzdvds  16721  pceq0  16797  pc2dvds  16805  fldivp1  16823  pcfac  16825  prmreclem3  16844  1arith  16853  4sqlem10  16873  4sqlem17  16887  4sqlem18  16888  vdwlem6  16912  ramubcl  16944  ramcl  16955  mrissmrcd  17561  psgnunilem5  19421  oddvdsnn0  19471  odnncl  19472  oddvds  19474  odcl2  19492  gexdvds  19511  gexnnod  19515  sylow1lem1  19525  odcau  19531  pgpssslw  19541  efgs1b  19663  efgredlema  19667  torsubg  19781  prmcyg  19821  gsumval3eu  19831  ablfacrplem  19994  ablfac1eu  20002  ablsimpgprmd  20044  fidomndrnglem  20703  lspdisj  21078  lspsncv0  21099  gzrngunitlem  21385  prmirredlem  21425  fctop  22946  cctop  22948  ppttop  22949  pptbas  22950  ordtrest2lem  23145  connclo  23357  txindis  23576  filconn  23825  ufilb  23848  cldsubg  24053  reconnlem1  24769  reconnlem2  24770  metds0  24793  metdseq0  24797  metnrmlem1a  24801  iccpnfhmeo  24897  xrhmeo  24898  cphsubrglem  25131  minveclem3b  25382  minveclem4a  25384  vitalilem4  25566  itg2gt0  25715  itgsplitioo  25793  limccnp2  25847  rollelem  25947  dvlip  25952  itgsubstlem  26009  plyaddlem1  26172  plymullem1  26173  coefv0  26207  dgreq0  26225  radcnv0  26379  pserdvlem2  26392  pilem2  26416  sineq0  26487  logtayl  26623  cxpsqrt  26666  isosctrlem2  26783  atantayl2  26902  rlimcnp2  26930  amgm  26955  basellem3  27047  muval2  27098  sqf11  27103  ppinprm  27116  chtnprm  27118  perfectlem2  27195  lgsdir  27297  lgsabs1  27301  lgseisenlem1  27340  2sqlem7  27389  2sqblem  27396  2sqmod  27401  2sqreultblem  27413  2sqreunnltblem  27416  chebbnd1lem1  27434  dchrisum0flblem1  27473  pntpbnd1  27551  pntpbnd2  27552  ostth  27604  nosepon  27631  abssge0  28213  elnns2  28301  dfnns2  28330  symquadlem  28710  midexlem  28713  colperp  28750  midex  28758  oppperpex  28774  hlpasch  28777  hpgerlem  28786  colopp  28790  lmieu  28805  lmicom  28809  trgcopy  28825  cgracol  28849  minvecolem5  30905  staddi  32270  stadd3i  32272  atsseq  32371  atom1d  32377  atoml2i  32407  disji2f  32601  disjif2  32605  fprodex01  32855  sgn3da  32864  psgnfzto1stlem  33131  lvecdim0  33712  ordtrest2NEWlem  34028  eulerpartlemb  34474  subfacp1lem6  35328  cvmscld  35416  cvmsss2  35417  cvmseu  35419  ordtoplem  36578  ordcmp  36590  poimirlem25  37785  heiborlem6  37956  isfldidl  38208  pridlc2  38212  mpobi123f  38302  mptbi12f  38306  ac6s6  38312  lsatcmp  39202  lsatcmp2  39203  2atm  39726  trlatn0  40371  trlval3  40386  cdleme18c  40492  cdlemg17b  40861  cdlemg17i  40868  cdlemh  41016  dia2dimlem2  41264  dia2dimlem3  41265  dochlkr  41584  dochkrshp  41585  lcfl6  41699  lcfrlem9  41749  hdmap14lem6  42072  hgmapval0  42091  ioin9i8  42400  ctbnfien  43002  pw2f1ocnv  43221  unxpwdom3  43279  dgrsub2  43319  dflim5  43513  rp-fakeanorass  43696  mnuprdlem1  44455  mnuprdlem2  44456  mnurndlem1  44464  disjxp1  45256  fmul01lt1lem1  45772  stoweidlem35  46221  stirlinglem5  46264  stirlinglem12  46271  fourierdlem42  46335  fourierdlem93  46385  perfectALTVlem2  47910