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  ecase23d  1472  19.33b  1882  elpwunsn  4688  disji2  5131  disjxiun  5144  pwssun  5579  swopo  5607  sotric  5625  sotrieq  5626  somo  5634  ordtri3or  6417  ordtri1  6418  suc11  6492  foconst  6835  ordeleqon  7800  ssonprc  7806  onmindif2  7826  limsssuc  7870  limom  7902  onfununi  8379  oeeulem  8637  uniinqs  8835  pw2f1olem  9114  pssnn  9206  ordtypelem9  9563  ordtypelem10  9564  oismo  9577  preleqALT  9654  suc11reg  9656  cantnfp1lem2  9716  cantnflem1  9726  cnfcom2lem  9738  cnfcom3lem  9740  rankxpsuc  9919  cardlim  10009  alephdom  10118  cardaleph  10126  iscard3  10130  pwdjudom  10252  cfslbn  10304  fin1a2lem12  10448  gchi  10661  tskssel  10794  inttsk  10811  inar1  10812  r1tskina  10819  tskuni  10820  gruina  10855  grur1  10857  nlt1pi  10943  nqereu  10966  leltne  11347  nneo  12699  zeo2  12702  xrleltne  13183  nltpnft  13202  ngtmnft  13204  xrrebnd  13206  xaddf  13262  xrsupsslem  13345  xrinfmsslem  13346  fzocatel  13764  seqf1olem1  14078  seqf1olem2  14079  znsqcld  14198  discr1  14274  hashnncl  14401  seqcoll2  14500  sqeqd  15201  sqrmo  15286  isercoll  15700  bitsfzo  16468  bitsinv1lem  16474  bitsf1  16479  bezoutlem3  16574  eucalglt  16618  phibndlem  16803  dfphi2  16807  prmdiv  16818  odzdvds  16828  pceq0  16904  pc2dvds  16912  fldivp1  16930  pcfac  16932  prmreclem3  16951  1arith  16960  4sqlem10  16980  4sqlem17  16994  4sqlem18  16995  vdwlem6  17019  ramubcl  17051  ramcl  17062  mrissmrcd  17684  psgnunilem5  19526  oddvdsnn0  19576  odnncl  19577  oddvds  19579  odcl2  19597  gexdvds  19616  gexnnod  19620  sylow1lem1  19630  odcau  19636  pgpssslw  19646  efgs1b  19768  efgredlema  19772  torsubg  19886  prmcyg  19926  gsumval3eu  19936  ablfacrplem  20099  ablfac1eu  20107  ablsimpgprmd  20149  fidomndrnglem  20789  lspdisj  21144  lspsncv0  21165  gzrngunitlem  21467  prmirredlem  21500  fctop  23026  cctop  23028  ppttop  23029  pptbas  23030  ordtrest2lem  23226  connclo  23438  txindis  23657  filconn  23906  ufilb  23929  cldsubg  24134  reconnlem1  24861  reconnlem2  24862  metds0  24885  metdseq0  24889  metnrmlem1a  24893  iccpnfhmeo  24989  xrhmeo  24990  cphsubrglem  25224  minveclem3b  25475  minveclem4a  25477  vitalilem4  25659  itg2gt0  25809  itgsplitioo  25887  limccnp2  25941  rollelem  26041  dvlip  26046  itgsubstlem  26103  plyaddlem1  26266  plymullem1  26267  coefv0  26301  dgreq0  26319  radcnv0  26473  pserdvlem2  26486  pilem2  26510  sineq0  26580  logtayl  26716  cxpsqrt  26759  isosctrlem2  26876  atantayl2  26995  rlimcnp2  27023  amgm  27048  basellem3  27140  muval2  27191  sqf11  27196  ppinprm  27209  chtnprm  27211  perfectlem2  27288  lgsdir  27390  lgsabs1  27394  lgseisenlem1  27433  2sqlem7  27482  2sqblem  27489  2sqmod  27494  2sqreultblem  27506  2sqreunnltblem  27509  chebbnd1lem1  27527  dchrisum0flblem1  27566  pntpbnd1  27644  pntpbnd2  27645  ostth  27697  nosepon  27724  abssge0  28283  elnns2  28358  dfnns2  28376  symquadlem  28711  midexlem  28714  colperp  28751  midex  28759  oppperpex  28775  hlpasch  28778  hpgerlem  28787  colopp  28791  lmieu  28806  lmicom  28810  trgcopy  28826  cgracol  28850  minvecolem5  30909  staddi  32274  stadd3i  32276  atsseq  32375  atom1d  32381  atoml2i  32411  disji2f  32596  disjif2  32600  fprodex01  32831  psgnfzto1stlem  33102  lvecdim0  33633  ordtrest2NEWlem  33882  eulerpartlemb  34349  sgn3da  34522  subfacp1lem6  35169  cvmscld  35257  cvmsss2  35258  cvmseu  35260  ordtoplem  36417  ordcmp  36429  poimirlem25  37631  heiborlem6  37802  isfldidl  38054  pridlc2  38058  mpobi123f  38148  mptbi12f  38152  ac6s6  38158  lsatcmp  38984  lsatcmp2  38985  2atm  39509  trlatn0  40154  trlval3  40169  cdleme18c  40275  cdlemg17b  40644  cdlemg17i  40651  cdlemh  40799  dia2dimlem2  41047  dia2dimlem3  41048  dochlkr  41367  dochkrshp  41368  lcfl6  41482  lcfrlem9  41532  hdmap14lem6  41855  hgmapval0  41874  ioin9i8  42225  ctbnfien  42805  pw2f1ocnv  43025  unxpwdom3  43083  dgrsub2  43123  dflim5  43318  rp-fakeanorass  43502  mnuprdlem1  44267  mnuprdlem2  44268  mnurndlem1  44276  disjxp1  45008  fmul01lt1lem1  45539  elprn1  45588  stoweidlem35  45990  stirlinglem5  46033  stirlinglem12  46040  fourierdlem42  46104  fourierdlem93  46154  perfectALTVlem2  47646