Theorem ord 878

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  olcnd  891  orcanai  1018  ecase2d  1047  oplem1  1072  ornld  1077  19.33b  1918  elpwunsn  4645  disji2  5087  disjxiun  5100  pwssun  5547  swopo  5574  sotric  5593  sotrieq  5594  somo  5602  ordtri3or  6390  ordtri1  6391  suc11  6467  foconst  6805  ordeleqon  7782  ssonprc  7787  onmindif2  7807  limsssuc  7847  limom  7879  onfununi  8331  oeeulem  8592  uniinqs  8800  pw2f1olem  9082  pssnn  9166  ordtypelem9  9501  ordtypelem10  9502  oismo  9515  preleqALT  9599  suc11reg  9601  cantnfp1lem2  9661  cantnflem1  9671  cnfcom2lem  9683  cnfcom3lem  9685  rankxpsuc  9867  cardlim  9980  alephdom  10087  cardaleph  10095  iscard3  10099  pwdjudom  10220  cfslbn  10272  fin1a2lem12  10416  gchi  10636  tskssel  10769  inttsk  10786  inar1  10787  r1tskina  10794  tskuni  10795  gruina  10830  grur1  10832  nlt1pi  10918  nqereu  10941  leltne  11326  nneo  12708  zeo2  12711  xrleltne  13199  nltpnft  13219  ngtmnft  13221  xrrebnd  13223  xaddf  13279  xrsupsslem  13362  xrinfmsslem  13363  fzocatel  13788  seqf1olem1  14108  seqf1olem2  14109  znsqcld  14229  discr1  14306  hashnncl  14433  seqcoll2  14533  sgn3da  15177  sqeqd  15256  sqrmo  15341  isercoll  15758  bitsfzo  16528  bitsinv1lem  16534  bitsf1  16539  bezoutlem3  16634  eucalglt  16678  phibndlem  16864  dfphi2  16868  prmdiv  16879  odzdvds  16890  pceq0  16966  pc2dvds  16974  fldivp1  16992  pcfac  16994  prmreclem3  17013  1arith  17022  4sqlem10  17042  4sqlem17  17056  4sqlem18  17057  vdwlem6  17081  ramubcl  17113  ramcl  17124  mrissmrcd  17731  psgnunilem5  19624  oddvdsnn0  19674  odnncl  19675  oddvds  19677  odcl2  19695  gexdvds  19714  gexnnod  19718  sylow1lem1  19728  odcau  19734  pgpssslw  19744  efgs1b  19866  efgredlema  19870  torsubg  19984  prmcyg  20024  gsumval3eu  20034  ablfacrplem  20197  ablfac1eu  20205  ablsimpgprmd  20247  fidomndrnglem  20942  lspdisj  21315  lspsncv0  21336  prmidlc2  21540  gzrngunitlem  21648  prmirredlem  21688  fctop  23232  cctop  23234  ppttop  23235  pptbas  23236  ordtrest2lem  23431  connclo  23643  txindis  23863  filconn  24112  ufilb  24135  cldsubg  24340  reconnlem1  25056  reconnlem2  25057  metds0  25080  metdseq0  25084  metnrmlem1a  25088  iccpnfhmeo  25176  xrhmeo  25177  cphsubrglem  25408  minveclem3b  25659  minveclem4a  25661  vitalilem4  25842  itg2gt0  25991  itgsplitioo  26068  limccnp2  26122  rollelem  26219  dvlip  26223  itgsubstlem  26278  plyaddlem1  26442  plymullem1  26443  coefv0  26477  dgreq0  26494  radcnv0  26655  pserdvlem2  26667  pilem2  26691  sineq0  26764  logtayl  26900  cxpsqrt  26943  isosctrlem2  27059  atantayl2  27178  rlimcnp2  27206  amgm  27230  basellem3  27322  muval2  27373  sqf11  27378  chtnprm  27393  perfectlem2  27469  lgsdir  27571  lgsabs1  27575  lgseisenlem1  27614  2sqlem7  27663  2sqblem  27670  2sqmod  27675  2sqreultblem  27687  2sqreunnltblem  27690  chebbnd1lem1  27708  dchrisum0flblem1  27747  pntpbnd1  27825  pntpbnd2  27826  ostth  27878  nosepon  27904  abssge0  28513  elnns2  28609  dfnns2  28640  z12bday  28753  symquadlem  29043  midexlem  29046  colperp  29087  midex  29095  oppperpex  29111  hlpasch  29116  hpgerlem  29125  colopp  29129  plngrotlem1  29147  lmieu  29171  lmicom  29175  trgcopy  29193  cgracol  29218  minvecolem5  31365  staddi  32730  stadd3i  32732  atsseq  32831  atom1d  32837  atoml2i  32867  disji2f  33053  disjif2  33057  fprodex01  33298  psgnfzto1stlem  33543  lvecdim0  34120  ordtrest2NEWlem  34435  eulerpartlemb  34882  subfacp1lem6  35767  cvmscld  35855  cvmsss2  35856  cvmseu  35858  ordtoplem  37057  ordcmp  37069  poimirlem25  38397  heiborlem6  38569  isfldidl  38821  pridlc2  38825  mpobi123f  38913  mptbi12f  38917  ac6s6  38923  lsatcmp  39879  lsatcmp2  39880  2atm  40403  trlatn0  41048  trlval3  41063  cdleme18c  41169  cdlemg17b  41538  cdlemg17i  41545  cdlemh  41693  dia2dimlem2  41941  dia2dimlem3  41942  dochlkr  42261  dochkrshp  42262  lcfl6  42376  lcfrlem9  42426  hdmap14lem6  42749  hgmapval0  42768  ioin9i8  43078  ctbnfien  43662  pw2f1ocnv  43881  unxpwdom3  43939  dgrsub2  43979  dflim5  44173  rp-fakeanorass  44356  mnuprdlem1  45099  mnuprdlem2  45100  mnurndlem1  45108  disjxp1  45906  fmul01lt1lem1  46417  stoweidlem35  46866  stirlinglem5  46909  stirlinglem12  46916  fourierdlem42  46980  fourierdlem93  47030  perfectALTVlem2  48641