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  1885  elpwunsn  4636  disji2  5076  disjxiun  5089  pwssun  5511  swopo  5538  sotric  5557  sotrieq  5558  somo  5566  ordtri3or  6339  ordtri1  6340  suc11  6416  foconst  6751  ordeleqon  7718  ssonprc  7723  onmindif2  7743  limsssuc  7783  limom  7815  onfununi  8264  oeeulem  8519  uniinqs  8724  pw2f1olem  8998  pssnn  9082  ordtypelem9  9418  ordtypelem10  9419  oismo  9432  preleqALT  9513  suc11reg  9515  cantnfp1lem2  9575  cantnflem1  9585  cnfcom2lem  9597  cnfcom3lem  9599  rankxpsuc  9778  cardlim  9868  alephdom  9975  cardaleph  9983  iscard3  9987  pwdjudom  10109  cfslbn  10161  fin1a2lem12  10305  gchi  10518  tskssel  10651  inttsk  10668  inar1  10669  r1tskina  10676  tskuni  10677  gruina  10712  grur1  10714  nlt1pi  10800  nqereu  10823  leltne  11205  nneo  12560  zeo2  12563  xrleltne  13047  nltpnft  13066  ngtmnft  13068  xrrebnd  13070  xaddf  13126  xrsupsslem  13209  xrinfmsslem  13210  fzocatel  13632  seqf1olem1  13948  seqf1olem2  13949  znsqcld  14069  discr1  14146  hashnncl  14273  seqcoll2  14372  sqeqd  15073  sqrmo  15158  isercoll  15575  bitsfzo  16346  bitsinv1lem  16352  bitsf1  16357  bezoutlem3  16452  eucalglt  16496  phibndlem  16681  dfphi2  16685  prmdiv  16696  odzdvds  16707  pceq0  16783  pc2dvds  16791  fldivp1  16809  pcfac  16811  prmreclem3  16830  1arith  16839  4sqlem10  16859  4sqlem17  16873  4sqlem18  16874  vdwlem6  16898  ramubcl  16930  ramcl  16941  mrissmrcd  17546  psgnunilem5  19373  oddvdsnn0  19423  odnncl  19424  oddvds  19426  odcl2  19444  gexdvds  19463  gexnnod  19467  sylow1lem1  19477  odcau  19483  pgpssslw  19493  efgs1b  19615  efgredlema  19619  torsubg  19733  prmcyg  19773  gsumval3eu  19783  ablfacrplem  19946  ablfac1eu  19954  ablsimpgprmd  19996  fidomndrnglem  20657  lspdisj  21032  lspsncv0  21053  gzrngunitlem  21339  prmirredlem  21379  fctop  22889  cctop  22891  ppttop  22892  pptbas  22893  ordtrest2lem  23088  connclo  23300  txindis  23519  filconn  23768  ufilb  23791  cldsubg  23996  reconnlem1  24713  reconnlem2  24714  metds0  24737  metdseq0  24741  metnrmlem1a  24745  iccpnfhmeo  24841  xrhmeo  24842  cphsubrglem  25075  minveclem3b  25326  minveclem4a  25328  vitalilem4  25510  itg2gt0  25659  itgsplitioo  25737  limccnp2  25791  rollelem  25891  dvlip  25896  itgsubstlem  25953  plyaddlem1  26116  plymullem1  26117  coefv0  26151  dgreq0  26169  radcnv0  26323  pserdvlem2  26336  pilem2  26360  sineq0  26431  logtayl  26567  cxpsqrt  26610  isosctrlem2  26727  atantayl2  26846  rlimcnp2  26874  amgm  26899  basellem3  26991  muval2  27042  sqf11  27047  ppinprm  27060  chtnprm  27062  perfectlem2  27139  lgsdir  27241  lgsabs1  27245  lgseisenlem1  27284  2sqlem7  27333  2sqblem  27340  2sqmod  27345  2sqreultblem  27357  2sqreunnltblem  27360  chebbnd1lem1  27378  dchrisum0flblem1  27417  pntpbnd1  27495  pntpbnd2  27496  ostth  27548  nosepon  27575  abssge0  28154  elnns2  28240  dfnns2  28268  symquadlem  28638  midexlem  28641  colperp  28678  midex  28686  oppperpex  28702  hlpasch  28705  hpgerlem  28714  colopp  28718  lmieu  28733  lmicom  28737  trgcopy  28753  cgracol  28777  minvecolem5  30829  staddi  32194  stadd3i  32196  atsseq  32295  atom1d  32301  atoml2i  32331  disji2f  32526  disjif2  32530  fprodex01  32779  sgn3da  32788  psgnfzto1stlem  33051  lvecdim0  33589  ordtrest2NEWlem  33905  eulerpartlemb  34352  subfacp1lem6  35178  cvmscld  35266  cvmsss2  35267  cvmseu  35269  ordtoplem  36429  ordcmp  36441  poimirlem25  37645  heiborlem6  37816  isfldidl  38068  pridlc2  38072  mpobi123f  38162  mptbi12f  38166  ac6s6  38172  lsatcmp  39002  lsatcmp2  39003  2atm  39526  trlatn0  40171  trlval3  40186  cdleme18c  40292  cdlemg17b  40661  cdlemg17i  40668  cdlemh  40816  dia2dimlem2  41064  dia2dimlem3  41065  dochlkr  41384  dochkrshp  41385  lcfl6  41499  lcfrlem9  41549  hdmap14lem6  41872  hgmapval0  41891  ioin9i8  42200  ctbnfien  42811  pw2f1ocnv  43030  unxpwdom3  43088  dgrsub2  43128  dflim5  43322  rp-fakeanorass  43506  mnuprdlem1  44265  mnuprdlem2  44266  mnurndlem1  44274  disjxp1  45067  fmul01lt1lem1  45585  elprn1  45634  stoweidlem35  46036  stirlinglem5  46079  stirlinglem12  46086  fourierdlem42  46150  fourierdlem93  46200  perfectALTVlem2  47726