Theorem ord 865

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

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

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 849

This theorem is referenced by:  olcnd  878  orcanai  1005  ecase2d  1032  oplem1  1057  ornld  1062  19.33b  1887  elpwunsn  4643  disji2  5084  disjxiun  5097  pwssun  5526  swopo  5553  sotric  5572  sotrieq  5573  somo  5581  ordtri3or  6359  ordtri1  6360  suc11  6436  foconst  6771  ordeleqon  7739  ssonprc  7744  onmindif2  7764  limsssuc  7804  limom  7836  onfununi  8285  oeeulem  8541  uniinqs  8748  pw2f1olem  9023  pssnn  9107  ordtypelem9  9445  ordtypelem10  9446  oismo  9459  preleqALT  9540  suc11reg  9542  cantnfp1lem2  9602  cantnflem1  9612  cnfcom2lem  9624  cnfcom3lem  9626  rankxpsuc  9808  cardlim  9898  alephdom  10005  cardaleph  10013  iscard3  10017  pwdjudom  10139  cfslbn  10191  fin1a2lem12  10335  gchi  10549  tskssel  10682  inttsk  10699  inar1  10700  r1tskina  10707  tskuni  10708  gruina  10743  grur1  10745  nlt1pi  10831  nqereu  10854  leltne  11236  nneo  12590  zeo2  12593  xrleltne  13073  nltpnft  13093  ngtmnft  13095  xrrebnd  13097  xaddf  13153  xrsupsslem  13236  xrinfmsslem  13237  fzocatel  13659  seqf1olem1  13978  seqf1olem2  13979  znsqcld  14099  discr1  14176  hashnncl  14303  seqcoll2  14402  sqeqd  15103  sqrmo  15188  isercoll  15605  bitsfzo  16376  bitsinv1lem  16382  bitsf1  16387  bezoutlem3  16482  eucalglt  16526  phibndlem  16711  dfphi2  16715  prmdiv  16726  odzdvds  16737  pceq0  16813  pc2dvds  16821  fldivp1  16839  pcfac  16841  prmreclem3  16860  1arith  16869  4sqlem10  16889  4sqlem17  16903  4sqlem18  16904  vdwlem6  16928  ramubcl  16960  ramcl  16971  mrissmrcd  17577  psgnunilem5  19440  oddvdsnn0  19490  odnncl  19491  oddvds  19493  odcl2  19511  gexdvds  19530  gexnnod  19534  sylow1lem1  19544  odcau  19550  pgpssslw  19560  efgs1b  19682  efgredlema  19686  torsubg  19800  prmcyg  19840  gsumval3eu  19850  ablfacrplem  20013  ablfac1eu  20021  ablsimpgprmd  20063  fidomndrnglem  20722  lspdisj  21097  lspsncv0  21118  gzrngunitlem  21404  prmirredlem  21444  fctop  22965  cctop  22967  ppttop  22968  pptbas  22969  ordtrest2lem  23164  connclo  23376  txindis  23595  filconn  23844  ufilb  23867  cldsubg  24072  reconnlem1  24788  reconnlem2  24789  metds0  24812  metdseq0  24816  metnrmlem1a  24820  iccpnfhmeo  24916  xrhmeo  24917  cphsubrglem  25150  minveclem3b  25401  minveclem4a  25403  vitalilem4  25585  itg2gt0  25734  itgsplitioo  25812  limccnp2  25866  rollelem  25966  dvlip  25971  itgsubstlem  26028  plyaddlem1  26191  plymullem1  26192  coefv0  26226  dgreq0  26244  radcnv0  26398  pserdvlem2  26411  pilem2  26435  sineq0  26506  logtayl  26642  cxpsqrt  26685  isosctrlem2  26802  atantayl2  26921  rlimcnp2  26949  amgm  26974  basellem3  27066  muval2  27117  sqf11  27122  ppinprm  27135  chtnprm  27137  perfectlem2  27214  lgsdir  27316  lgsabs1  27320  lgseisenlem1  27359  2sqlem7  27408  2sqblem  27415  2sqmod  27420  2sqreultblem  27432  2sqreunnltblem  27435  chebbnd1lem1  27453  dchrisum0flblem1  27492  pntpbnd1  27570  pntpbnd2  27571  ostth  27623  nosepon  27650  abssge0  28258  elnns2  28354  dfnns2  28385  z12bday  28498  symquadlem  28779  midexlem  28782  colperp  28819  midex  28827  oppperpex  28843  hlpasch  28846  hpgerlem  28855  colopp  28859  lmieu  28874  lmicom  28878  trgcopy  28894  cgracol  28918  minvecolem5  30975  staddi  32340  stadd3i  32342  atsseq  32441  atom1d  32447  atoml2i  32477  disji2f  32670  disjif2  32674  fprodex01  32923  sgn3da  32932  psgnfzto1stlem  33200  lvecdim0  33790  ordtrest2NEWlem  34106  eulerpartlemb  34552  subfacp1lem6  35407  cvmscld  35495  cvmsss2  35496  cvmseu  35498  ordtoplem  36657  ordcmp  36669  poimirlem25  37925  heiborlem6  38096  isfldidl  38348  pridlc2  38352  mpobi123f  38442  mptbi12f  38446  ac6s6  38452  lsatcmp  39408  lsatcmp2  39409  2atm  39932  trlatn0  40577  trlval3  40592  cdleme18c  40698  cdlemg17b  41067  cdlemg17i  41074  cdlemh  41222  dia2dimlem2  41470  dia2dimlem3  41471  dochlkr  41790  dochkrshp  41791  lcfl6  41905  lcfrlem9  41955  hdmap14lem6  42278  hgmapval0  42297  ioin9i8  42606  ctbnfien  43204  pw2f1ocnv  43423  unxpwdom3  43481  dgrsub2  43521  dflim5  43715  rp-fakeanorass  43898  mnuprdlem1  44657  mnuprdlem2  44658  mnurndlem1  44666  disjxp1  45458  fmul01lt1lem1  45973  stoweidlem35  46422  stirlinglem5  46465  stirlinglem12  46472  fourierdlem42  46536  fourierdlem93  46586  perfectALTVlem2  48111