Theorem ord 877

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

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

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 210  df-or 861

This theorem is referenced by:  olcnd  890  orcanai  1018  ecase2d  1045  oplem1  1070  ornld  1075  19.33b  1912  elpwunsn  4655  disji2  5097  disjxiun  5110  pwssun  5554  swopo  5581  sotric  5600  sotrieq  5601  somo  5609  ordtri3or  6394  ordtri1  6395  suc11  6471  foconst  6808  ordeleqon  7781  ssonprc  7786  onmindif2  7806  limsssuc  7846  limom  7878  onfununi  8328  oeeulem  8587  uniinqs  8795  pw2f1olem  9069  pssnn  9153  ordtypelem9  9488  ordtypelem10  9489  oismo  9502  preleqALT  9586  suc11reg  9588  cantnfp1lem2  9648  cantnflem1  9658  cnfcom2lem  9670  cnfcom3lem  9672  rankxpsuc  9854  cardlim  9958  alephdom  10065  cardaleph  10073  iscard3  10077  pwdjudom  10198  cfslbn  10251  fin1a2lem12  10395  gchi  10609  tskssel  10742  inttsk  10759  inar1  10760  r1tskina  10767  tskuni  10768  gruina  10803  grur1  10805  nlt1pi  10891  nqereu  10914  leltne  11299  nneo  12680  zeo2  12683  xrleltne  13170  nltpnft  13190  ngtmnft  13192  xrrebnd  13194  xaddf  13250  xrsupsslem  13333  xrinfmsslem  13334  fzocatel  13758  seqf1olem1  14077  seqf1olem2  14078  znsqcld  14198  discr1  14275  hashnncl  14402  seqcoll2  14502  sgn3da  15138  sqeqd  15217  sqrmo  15302  isercoll  15719  bitsfzo  16493  bitsinv1lem  16499  bitsf1  16504  bezoutlem3  16599  eucalglt  16643  phibndlem  16829  dfphi2  16833  prmdiv  16844  odzdvds  16855  pceq0  16931  pc2dvds  16939  fldivp1  16957  pcfac  16959  prmreclem3  16978  1arith  16987  4sqlem10  17007  4sqlem17  17021  4sqlem18  17022  vdwlem6  17046  ramubcl  17078  ramcl  17089  mrissmrcd  17696  psgnunilem5  19564  oddvdsnn0  19614  odnncl  19615  oddvds  19617  odcl2  19635  gexdvds  19654  gexnnod  19658  sylow1lem1  19668  odcau  19674  pgpssslw  19684  efgs1b  19806  efgredlema  19810  torsubg  19924  prmcyg  19964  gsumval3eu  19974  ablfacrplem  20137  ablfac1eu  20145  ablsimpgprmd  20187  fidomndrnglem  20854  lspdisj  21227  lspsncv0  21248  gzrngunitlem  21551  prmirredlem  21591  fctop  23130  cctop  23132  ppttop  23133  pptbas  23134  ordtrest2lem  23329  connclo  23541  txindis  23760  filconn  24009  ufilb  24032  cldsubg  24237  reconnlem1  24953  reconnlem2  24954  metds0  24977  metdseq0  24981  metnrmlem1a  24985  iccpnfhmeo  25073  xrhmeo  25074  cphsubrglem  25305  minveclem3b  25556  minveclem4a  25558  vitalilem4  25739  itg2gt0  25888  itgsplitioo  25966  limccnp2  26020  rollelem  26117  dvlip  26121  itgsubstlem  26176  plyaddlem1  26339  plymullem1  26340  coefv0  26374  dgreq0  26391  radcnv0  26545  pserdvlem2  26557  pilem2  26581  sineq0  26655  logtayl  26791  cxpsqrt  26834  isosctrlem2  26950  atantayl2  27069  rlimcnp2  27097  amgm  27121  basellem3  27213  muval2  27264  sqf11  27269  ppinprm  27282  chtnprm  27284  perfectlem2  27360  lgsdir  27462  lgsabs1  27466  lgseisenlem1  27505  2sqlem7  27554  2sqblem  27561  2sqmod  27566  2sqreultblem  27578  2sqreunnltblem  27581  chebbnd1lem1  27599  dchrisum0flblem1  27638  pntpbnd1  27716  pntpbnd2  27717  ostth  27769  nosepon  27795  abssge0  28404  elnns2  28500  dfnns2  28531  z12bday  28644  symquadlem  28928  midexlem  28931  colperp  28969  midex  28977  oppperpex  28993  hlpasch  28997  hpgerlem  29006  colopp  29010  plngrotlem1  29027  lmieu  29051  lmicom  29055  trgcopy  29072  cgracol  29096  minvecolem5  31174  staddi  32539  stadd3i  32541  atsseq  32640  atom1d  32646  atoml2i  32676  disji2f  32863  disjif2  32867  fprodex01  33110  psgnfzto1stlem  33361  lvecdim0  33942  ordtrest2NEWlem  34257  eulerpartlemb  34703  subfacp1lem6  35610  cvmscld  35698  cvmsss2  35699  cvmseu  35701  ordtoplem  36869  ordcmp  36881  poimirlem25  38218  heiborlem6  38389  isfldidl  38641  pridlc2  38645  mpobi123f  38735  mptbi12f  38739  ac6s6  38745  lsatcmp  39701  lsatcmp2  39702  2atm  40225  trlatn0  40870  trlval3  40885  cdleme18c  40991  cdlemg17b  41360  cdlemg17i  41367  cdlemh  41515  dia2dimlem2  41763  dia2dimlem3  41764  dochlkr  42083  dochkrshp  42084  lcfl6  42198  lcfrlem9  42248  hdmap14lem6  42571  hgmapval0  42590  ioin9i8  42900  ctbnfien  43471  pw2f1ocnv  43690  unxpwdom3  43748  dgrsub2  43788  dflim5  43982  rp-fakeanorass  44165  mnuprdlem1  44908  mnuprdlem2  44909  mnurndlem1  44917  disjxp1  45715  fmul01lt1lem1  46226  stoweidlem35  46675  stirlinglem5  46718  stirlinglem12  46725  fourierdlem42  46789  fourierdlem93  46839  perfectALTVlem2  48410