Theorem ord 863

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

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

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 206  df-or 847

This theorem is referenced by:  olcnd  876  orcanai  1002  ecase2d  1029  oplem1  1056  ornld  1061  ecase23d  1474  19.33b  1889  elpwunsn  4688  disji2  5131  disjxiun  5146  pwssun  5572  swopo  5600  sotric  5617  sotrieq  5618  somo  5626  ordtri3or  6397  ordtri1  6398  suc11  6472  foconst  6821  ordeleqon  7769  ssonprc  7775  onmindif2  7795  limsssuc  7839  limom  7871  onfununi  8341  oeeulem  8601  uniinqs  8791  pw2f1olem  9076  pssnn  9168  pssnnOLD  9265  ordtypelem9  9521  ordtypelem10  9522  oismo  9535  preleqALT  9612  suc11reg  9614  cantnfp1lem2  9674  cantnflem1  9684  cnfcom2lem  9696  cnfcom3lem  9698  rankxpsuc  9877  cardlim  9967  alephdom  10076  cardaleph  10084  iscard3  10088  pwdjudom  10211  cfslbn  10262  fin1a2lem12  10406  gchi  10619  tskssel  10752  inttsk  10769  inar1  10770  r1tskina  10777  tskuni  10778  gruina  10813  grur1  10815  nlt1pi  10901  nqereu  10924  leltne  11303  nneo  12646  zeo2  12649  xrleltne  13124  nltpnft  13143  ngtmnft  13145  xrrebnd  13147  xaddf  13203  xrsupsslem  13286  xrinfmsslem  13287  fzocatel  13696  seqf1olem1  14007  seqf1olem2  14008  znsqcld  14127  discr1  14202  hashnncl  14326  seqcoll2  14426  sqeqd  15113  sqrmo  15198  isercoll  15614  bitsfzo  16376  bitsinv1lem  16382  bitsf1  16387  bezoutlem3  16483  eucalglt  16522  phibndlem  16703  dfphi2  16707  prmdiv  16718  odzdvds  16728  pceq0  16804  pc2dvds  16812  fldivp1  16830  pcfac  16832  prmreclem3  16851  1arith  16860  4sqlem10  16880  4sqlem17  16894  4sqlem18  16895  vdwlem6  16919  ramubcl  16951  ramcl  16962  mrissmrcd  17584  psgnunilem5  19362  oddvdsnn0  19412  odnncl  19413  oddvds  19415  odcl2  19433  gexdvds  19452  gexnnod  19456  sylow1lem1  19466  odcau  19472  pgpssslw  19482  efgs1b  19604  efgredlema  19608  torsubg  19722  prmcyg  19762  gsumval3eu  19772  ablfacrplem  19935  ablfac1eu  19943  ablsimpgprmd  19985  lspdisj  20738  lspsncv0  20759  fidomndrnglem  20925  gzrngunitlem  21010  prmirredlem  21042  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  ordtrest2lem  22707  connclo  22919  txindis  23138  filconn  23387  ufilb  23410  cldsubg  23615  reconnlem1  24342  reconnlem2  24343  metds0  24366  metdseq0  24370  metnrmlem1a  24374  iccpnfhmeo  24461  xrhmeo  24462  cphsubrglem  24694  minveclem3b  24945  minveclem4a  24947  vitalilem4  25128  itg2gt0  25278  itgsplitioo  25355  limccnp2  25409  rollelem  25506  dvlip  25510  itgsubstlem  25565  plyaddlem1  25727  plymullem1  25728  coefv0  25762  dgreq0  25779  radcnv0  25928  pserdvlem2  25940  pilem2  25964  sineq0  26033  logtayl  26168  cxpsqrt  26211  isosctrlem2  26324  atantayl2  26443  rlimcnp2  26471  amgm  26495  basellem3  26587  muval2  26638  sqf11  26643  ppinprm  26656  chtnprm  26658  perfectlem2  26733  lgsdir  26835  lgsabs1  26839  lgseisenlem1  26878  2sqlem7  26927  2sqblem  26934  2sqmod  26939  2sqreultblem  26951  2sqreunnltblem  26954  chebbnd1lem1  26972  dchrisum0flblem1  27011  pntpbnd1  27089  pntpbnd2  27090  ostth  27142  nosepon  27168  symquadlem  27940  midexlem  27943  colperp  27980  midex  27988  oppperpex  28004  hlpasch  28007  hpgerlem  28016  colopp  28020  lmieu  28035  lmicom  28039  trgcopy  28055  cgracol  28079  minvecolem5  30134  staddi  31499  stadd3i  31501  atsseq  31600  atom1d  31606  atoml2i  31636  disji2f  31808  disjif2  31812  fprodex01  32031  psgnfzto1stlem  32259  lvecdim0  32691  ordtrest2NEWlem  32902  eulerpartlemb  33367  sgn3da  33540  subfacp1lem6  34176  cvmscld  34264  cvmsss2  34265  cvmseu  34267  ordtoplem  35320  ordcmp  35332  poimirlem25  36513  heiborlem6  36684  isfldidl  36936  pridlc2  36940  mpobi123f  37030  mptbi12f  37034  ac6s6  37040  lsatcmp  37873  lsatcmp2  37874  2atm  38398  trlatn0  39043  trlval3  39058  cdleme18c  39164  cdlemg17b  39533  cdlemg17i  39540  cdlemh  39688  dia2dimlem2  39936  dia2dimlem3  39937  dochlkr  40256  dochkrshp  40257  lcfl6  40371  lcfrlem9  40421  hdmap14lem6  40744  hgmapval0  40763  ioin9i8  41024  ctbnfien  41556  pw2f1ocnv  41776  unxpwdom3  41837  dgrsub2  41877  dflim5  42079  rp-fakeanorass  42264  mnuprdlem1  43031  mnuprdlem2  43032  mnurndlem1  43040  disjxp1  43756  fmul01lt1lem1  44300  elprn1  44349  stoweidlem35  44751  stirlinglem5  44794  stirlinglem12  44801  fourierdlem42  44865  fourierdlem93  44915  perfectALTVlem2  46390