Theorem ord 870

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

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

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 208  df-or 854

This theorem is referenced by:  olcnd  883  orcanai  1010  ecase2d  1037  oplem1  1062  ornld  1067  19.33b  1892  elpwunsn  4617  disji2  5057  disjxiun  5070  pwssun  5511  swopo  5538  sotric  5557  sotrieq  5558  somo  5566  ordtri3or  6343  ordtri1  6344  suc11  6420  foconst  6755  ordeleqon  7726  ssonprc  7731  onmindif2  7751  limsssuc  7791  limom  7823  onfununi  8272  oeeulem  8528  uniinqs  8735  pw2f1olem  9010  pssnn  9094  ordtypelem9  9432  ordtypelem10  9433  oismo  9446  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  11227  nneo  12605  zeo2  12608  xrleltne  13088  nltpnft  13108  ngtmnft  13110  xrrebnd  13112  xaddf  13168  xrsupsslem  13251  xrinfmsslem  13252  fzocatel  13676  seqf1olem1  13995  seqf1olem2  13996  znsqcld  14116  discr1  14193  hashnncl  14320  seqcoll2  14419  sqeqd  15120  sqrmo  15205  isercoll  15622  bitsfzo  16396  bitsinv1lem  16402  bitsf1  16407  bezoutlem3  16502  eucalglt  16546  phibndlem  16732  dfphi2  16736  prmdiv  16747  odzdvds  16758  pceq0  16834  pc2dvds  16842  fldivp1  16860  pcfac  16862  prmreclem3  16881  1arith  16890  4sqlem10  16910  4sqlem17  16924  4sqlem18  16925  vdwlem6  16949  ramubcl  16981  ramcl  16992  mrissmrcd  17598  psgnunilem5  19461  oddvdsnn0  19511  odnncl  19512  oddvds  19514  odcl2  19532  gexdvds  19551  gexnnod  19555  sylow1lem1  19565  odcau  19571  pgpssslw  19581  efgs1b  19703  efgredlema  19707  torsubg  19821  prmcyg  19861  gsumval3eu  19871  ablfacrplem  20034  ablfac1eu  20042  ablsimpgprmd  20084  fidomndrnglem  20745  lspdisj  21119  lspsncv0  21140  gzrngunitlem  21408  prmirredlem  21448  fctop  22988  cctop  22990  ppttop  22991  pptbas  22992  ordtrest2lem  23187  connclo  23399  txindis  23618  filconn  23867  ufilb  23890  cldsubg  24095  reconnlem1  24811  reconnlem2  24812  metds0  24835  metdseq0  24839  metnrmlem1a  24843  iccpnfhmeo  24931  xrhmeo  24932  cphsubrglem  25163  minveclem3b  25414  minveclem4a  25416  vitalilem4  25597  itg2gt0  25746  itgsplitioo  25824  limccnp2  25878  rollelem  25975  dvlip  25979  itgsubstlem  26034  plyaddlem1  26197  plymullem1  26198  coefv0  26232  dgreq0  26249  radcnv0  26400  pserdvlem2  26412  pilem2  26436  sineq0  26507  logtayl  26643  cxpsqrt  26686  isosctrlem2  26802  atantayl2  26921  rlimcnp2  26949  amgm  26973  basellem3  27065  muval2  27116  sqf11  27121  ppinprm  27134  chtnprm  27136  perfectlem2  27212  lgsdir  27314  lgsabs1  27318  lgseisenlem1  27357  2sqlem7  27406  2sqblem  27413  2sqmod  27418  2sqreultblem  27430  2sqreunnltblem  27433  chebbnd1lem1  27451  dchrisum0flblem1  27490  pntpbnd1  27568  pntpbnd2  27569  ostth  27621  nosepon  27648  abssge0  28256  elnns2  28352  dfnns2  28383  z12bday  28496  symquadlem  28776  midexlem  28779  colperp  28816  midex  28824  oppperpex  28840  hlpasch  28843  hpgerlem  28852  colopp  28856  lmieu  28871  lmicom  28875  trgcopy  28891  cgracol  28915  minvecolem5  30971  staddi  32336  stadd3i  32338  atsseq  32437  atom1d  32443  atoml2i  32473  disji2f  32667  disjif2  32671  fprodex01  32918  sgn3da  32927  psgnfzto1stlem  33182  lvecdim0  33800  ordtrest2NEWlem  34115  eulerpartlemb  34561  subfacp1lem6  35422  cvmscld  35510  cvmsss2  35511  cvmseu  35513  ordtoplem  36672  ordcmp  36684  poimirlem25  38021  heiborlem6  38192  isfldidl  38444  pridlc2  38448  mpobi123f  38538  mptbi12f  38542  ac6s6  38548  lsatcmp  39504  lsatcmp2  39505  2atm  40028  trlatn0  40673  trlval3  40688  cdleme18c  40794  cdlemg17b  41163  cdlemg17i  41170  cdlemh  41318  dia2dimlem2  41566  dia2dimlem3  41567  dochlkr  41886  dochkrshp  41887  lcfl6  42001  lcfrlem9  42051  hdmap14lem6  42374  hgmapval0  42393  ioin9i8  42701  ctbnfien  43272  pw2f1ocnv  43491  unxpwdom3  43549  dgrsub2  43589  dflim5  43783  rp-fakeanorass  43966  mnuprdlem1  44725  mnuprdlem2  44726  mnurndlem1  44734  disjxp1  45526  fmul01lt1lem1  46037  stoweidlem35  46486  stirlinglem5  46529  stirlinglem12  46536  fourierdlem42  46600  fourierdlem93  46650  perfectALTVlem2  48221