Theorem mpdan 697

Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
mpdan.1	⊢ (𝜑 → 𝜓)
mpdan.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpdan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpidan  699  mpan2  701  biadanid  832  mpjaodan  971  mpjao3dan  1453  mpd3an3  1484  elabd2  3630  eueq2  3674  csbiegf  3886  difsnb  4767  reusv3i  5362  frpoinsg  6330  fimadmfo  6787  fimadmfoALT  6789  fvtresfn  6978  fvmpt3  6980  ffvelcdmd  7066  fnressn  7141  fsnex  7267  f1oiso2  7336  riota5f  7381  onsuc  7793  onsucuni  7808  frrlem10  8276  seqomlem2  8422  oaordi  8515  nnaordi  8588  qsdisj  8776  dom2lem  8973  canth2g  9103  limenpsi  9124  nnfi  9136  php4  9178  onfin  9183  sucxpdom  9205  dmfi  9276  fiin  9366  supiso  9420  ordiso2  9461  wdom2d  9526  elirrvOLD  9544  infeq5  9590  cantnfp1lem3  9633  cantnflem1d  9641  rankwflemb  9749  onenon  9919  cardonle  9927  sdomsdomcardi  9941  acni  10013  cardaleph  10057  djuen  10137  djuinf  10156  infdju1  10157  nnadju  10165  pwsdompw  10170  infdif  10175  cfval  10214  fin34  10358  fin1a2lem1  10368  fin1a2  10383  ttukeylem6  10482  sdomsdomcard  10528  canth3  10529  fpwwe2  10612  canthwelem  10619  gchdju1  10625  pwfseqlem4  10631  gchdjuidm  10637  gchxpidm  10638  tskwe2  10742  rankcf  10746  tskuni  10752  gruxp  10776  dmrecnq  10937  lterpq  10939  archnq  10949  reclem3pr  11018  reclem4pr  11019  0idsr  11066  lep1  12043  ledivp1  12104  negfi  12151  supaddc  12169  supmul1  12171  suprzcl  12663  uz11  12874  zmin  12955  zbtwnre  12957  rpnnen1lem4  12991  rpnnen1lem5  12992  xnegid  13251  supxrre  13340  infxrre  13350  eluzfz2  13547  fzsuc  13586  fzsuc2  13597  fzp1disj  13598  fzneuz  13623  nn0p1elfzo  13718  fllep1  13821  fraclt1  13822  fracle1  13823  fracge0  13824  flhalf  13850  ceige  13864  ceim1l  13867  fldiv  13880  modval  13891  suppssfz  14017  seqeq1  14027  expubnd  14201  iexpcyc  14230  binom2sub1  14244  faclbnd4lem3  14318  pfxid  14708  pfxccatpfx2  14760  swrdccat3blem  14762  cshw0  14817  cshwn  14820  cshimadifsn  14852  cshimadifsn0  14853  pfx2  14970  trclexlem  15017  shftfval  15093  shftcan1  15106  sgnneg  15123  reval  15143  cjmulrcl  15181  addcj  15185  absval  15275  absneg  15314  abscj  15316  sqabsadd  15319  sqabssub  15320  leabs  15336  sqreulem  15397  lo1res  15596  o1of2  15650  o1rlimmul  15656  fsumconst1  15828  flo1  15894  trirecip  15903  efcan  16136  efi4p  16179  resin4p  16180  recos4p  16181  sincossq  16218  ruclem10  16281  iddvds  16313  1dvds  16314  2ebits  16491  lcmftp  16680  coprmgcdb  16693  1idssfct  16724  exprmfct  16749  eulerthlem2  16827  odzphi  16842  pcprendvds  16886  pcmpt  16938  oddprmdvds  16949  vdwlem8  17034  0ram2  17067  prmgaplem7  17103  setsn0fun  17219  setsexstruct2  17221  pwsvscaval  17535  2initoinv  18053  initoeu1  18054  initoeu2lem1  18057  initoeu2  18059  2termoinv  18060  termoeu1  18061  homarel  18079  joinfval  18413  meetfval  18427  latjcom  18489  latmcom  18505  0subm  18861  sgrp2nmndlem5  18976  grprcan  19025  isgrpid2  19028  grpinvid  19051  mulgnn0z  19153  qus0  19240  eqg0subg  19247  ghmker  19292  symgbasmap  19427  symginv  19452  pmtrfrn  19508  odmulg2  19605  slwpgp  19663  pj1eq  19750  efgtf  19772  frgpinv  19814  frgpup2  19826  cnaddablx  19918  cnaddabl  19919  zaddablx  19922  imasabl  19926  dprdfadd  20072  dpjidcl  20110  dpjlid  20113  pgpfac1lem3  20129  omndmul2  20183  omndmul  20185  rngen1zr0  20240  srgen1zr0  20276  1unit  20433  unitgrpid  20444  1rinv  20454  irredn0  20482  irredneg  20489  c0snmgmhm  20521  rngisomring1  20527  zrrnghm  20596  rnrhmsubrg  20665  zrinitorngc  20702  zrtermorngc  20703  zrtermoringc  20735  isdrng2  20802  abv0  20879  abv1z  20880  abvneg  20882  orng0le1  20930  lmodfopne  20974  lsssn0  21022  lspsn0  21082  lsp0  21083  lmhmvsca  21119  lmhmrnlss  21124  lmhmkerlss  21125  lsppratlem5  21228  rsp1  21314  kerlidl  21355  ring2idlqus  21386  rngqiprngfulem4  21391  rngqiprngfu  21394  cnfldneg  21457  zringcyg  21528  chrid  21584  chrrhm  21590  ip0r  21696  ocvlss  21731  ocv1  21738  rlmassa  21929  psrbagfsupp  21978  snifpsrbag  21979  psrbaglefi  21985  psrvscaval  22009  psrdi  22023  psrdir  22024  mplvscaval  22074  mhpmpl  22216  mhpdeg  22217  mhppwdeg  22222  psdmul  22238  psdpw  22242  coe1sclmulfv  22353  coe1id  22363  ply1idvr1OLD  22365  evl1var  22406  mamuvs1  22472  mamuvs2  22473  matecl  22492  matvscacell  22503  mat0scmat  22605  submaval0  22647  mdetrsca  22670  maduval  22705  minmar1val0  22714  pmatcollpw3fi1lem2  22854  chcoeffeqlem  22952  cayleyhamilton0  22956  cayleyhamiltonALT  22958  toponsspwpw  22989  cctop  23073  cldval  23090  ntrfval  23091  clsfval  23092  cmclsopn  23129  opncldf3  23153  neifval  23166  lpfval  23205  cnrmnrm  23428  dis2ndc  23527  islocfin  23584  tx1cn  23676  idqtop  23773  kqtopon  23794  kqid  23795  kqcld  23802  hmphen2  23866  filssufil  23979  ufileu  23986  alexsublem  24111  efmndtmd  24168  symgtgp  24173  ustuqtop4  24311  cstucnd  24350  metustexhalf  24623  nm0  24696  rlmnlm  24755  nmolb  24784  metdseq0  24922  pi1xfrval  25123  clmvneg1  25168  clmvsubval  25178  ipcau2  25303  tcphcphlem1  25304  tcphcphlem2  25305  cmetcaulem  25357  ovolicc2lem3  25588  ovolicc2lem4  25589  mbfmulc2lem  25716  i1fpos  25775  mbfi1fseqlem3  25786  itg2ge0  25804  bddiblnc  25911  dvres2  25981  dvaddbr  26007  dvmulbr  26008  dvcobr  26015  dvfsumlem4  26098  ftc1a  26106  ftc1lem6  26110  uc1pmon1p  26219  ig1pval2  26244  dgradd2  26335  dgrcolem2  26341  plydivlem4  26367  plydiveu  26369  elqaalem3  26392  qaa  26394  ulmdvlem1  26470  abelthlem6  26506  abelthlem7  26508  eflogeq  26674  jensenlem2  27059  harmonicbnd4  27082  sgmnncl  27218  dchrptlem2  27336  1lgs  27411  lgs1  27412  2sqcoprm  27506  addsqnreup  27514  dchrisumlem2  27561  dchrisum0lem2a  27588  selberg2lem  27621  pntrsumo1  27636  pntrsumbnd  27637  pntpbnd1  27657  pntlemr  27673  pntlemj  27674  padicabvf  27702  bdayval  27719  noextendgt  27741  nosupbnd2lem1  27786  noinfbnd2lem1  27801  noetainflem4  27811  oldval  27934  divmuls  28321  divscl  28323  seqsp1  28411  bdayfinbndlem1  28567  zz12s  28575  remulscllem1  28600  plngrotlem2  29002  incistruhgr  29287  subgrprop3  29484  subgruhgredgd  29492  usgrexi  29649  cusgrexi  29651  cusgrsizeinds  29660  vtxdgfusgrf  29705  1hevtxdg1  29714  1egrvtxdg1  29717  ewlkprop  29811  wlklenvm1  29829  wlkl1loop  29845  wlkp1lem4  29882  2pthnloop  29938  upgrclwlkcompim  29988  crctcshwlkn0lem4  30020  crctcshwlkn0lem5  30021  crctcshwlkn0lem6  30022  crctcshwlkn0lem7  30023  crctcshlem4  30027  wspthnonp  30066  wlkswwlksf1o  30086  wwlksnwwlksnon  30122  umgr2wlkon  30157  wwlks2onv  30160  elwwlks2ons3im  30161  elwspths2spth  30177  umgrclwwlkge2  30200  clwlkclwwlkf1lem3  30215  erclwwlkref  30229  clwwlknp  30246  wwlksext2clwwlk  30266  wwlksubclwwlk  30267  0pthon1  30337  1wlkdlem4  30349  1pthd  30352  3spthd  30385  eupth2eucrct  30426  eucrctshift  30452  eucrct2eupth  30454  frgrncvvdeqlem8  30515  frgr2wwlkeqm  30540  isgrpoi  30708  grpoinvfval  30732  grpodivfval  30744  vcz  30785  cnaddabloOLD  30791  nvz0  30878  sspz  30945  lno0  30966  nmobndi  30985  ipasslem2  31042  shunssi  31578  ococin  31618  ssjo  31657  pjocini  31908  nlfnval  32091  lncnopbd  32247  riesz3i  32272  cnlnadjlem7  32283  pjclem4  32409  pj3si  32417  hstoc  32432  hstnmoc  32433  hstoh  32442  hst0  32443  mdsl2i  32532  chirredlem3  32602  chirredlem4  32603  dmdbr5ati  32632  rexunirn  32697  fcnvgreu  32880  infxrge0glb  32973  cycpmco2lem5  33316  cycpmco2lem6  33317  cycpmco2lem7  33318  isarchi3  33373  rlocisunit  33463  nsgqusf1olem2  33603  ssdifidllem  33646  ssmxidllem  33664  rprmdvdspow  33732  ressply1sub  33769  selvply1rhmlemb  33818  fedgmullem1  33928  extdg1id  33965  nn0constr  34060  zartopn  34174  zarcmplem  34180  esumcvg  34385  esumcvgre  34390  sigaval  34410  unelldsys  34457  fiunelros  34473  measval  34497  pmeasmono  34623  probfinmeasb  34727  ballotlemfc0  34792  ballotlemfcc  34793  ballotlemsi  34814  ballotlemfrci  34827  signlem0  34883  breprexp  34929  bnj1006  35257  bnj1110  35279  bnj1253  35314  bnj1280  35317  bnj1463  35352  bnj1312  35355  fineqvinfep  35425  erdszelem7  35552  erdszelem8  35553  cvmliftlem10  35649  cvmliftlem13  35651  cvmlift2lem9  35666  cvmlift3lem6  35679  cvmlift3lem7  35680  cvmlift3lem9  35682  satfv1lem  35717  dfrdg2  36148  cldregopn  36696  tailfval  36737  filnetlem3  36745  filnetlem4  36746  ontopbas  36793  bj-nnfbd  37249  bj-elid4  37665  bj-imdiridlem  37682  f1omptsnlem  37835  icoreunrn  37858  relowlpssretop  37863  fvineqsnf1  37909  wl-sbal2  38072  unccur  38107  poimirlem1  38125  poimirlem2  38126  poimirlem4  38128  poimirlem6  38130  poimirlem7  38131  poimirlem11  38135  poimirlem12  38136  poimirlem17  38141  poimirlem20  38144  poimirlem22  38146  poimirlem23  38147  poimirlem28  38152  poimir  38157  ismblfin  38165  cnambfre  38172  ftc1cnnc  38196  dvasin  38208  ismtyres  38312  heiborlem8  38322  ghomidOLD  38393  rngosn6  38430  rngonegmn1l  38445  rngonegmn1r  38446  rngoneglmul  38447  rngonegrmul  38448  idlnegcl  38526  0idl  38529  0rngo  38531  smprngopr  38556  sucmapsuc  38993  cossex  39013  qsdisjALTV  39203  cnvepresdmqss  39241  mpets2  39459  lkrval  39717  ldualvaddval  39760  ldualvsval  39767  opoc1  39831  pmap0  40394  pmap1N  40396  pexmidALTN  40607  cdleme31fv  41019  cdlemg27b  41325  erngdvlem4  41620  erng0g  41623  erngdvlem4-rN  41628  dvalveclem  41654  dvh0g  41740  dih0cnv  41912  dih1rn  41916  dih1cnv  41917  doch0  41987  doch1  41988  lcfl7lem  42128  mapdheq  42357  hdmap1eq  42430  hdmapval2lem  42460  hgmapvvlem3  42554  zndvdchrrhm  42595  lcmineqlem13  42663  aks4d1p9  42710  primrootsunit1  42719  aks6d1c1p1  42729  aks6d1c1p6  42736  aks6d1c1p8  42737  sticksstones1  42768  sticksstones6  42773  sticksstones7  42774  sticksstones11  42778  sticksstones12a  42779  sticksstones12  42780  sticksstones22  42790  aks6d1c6isolem1  42796  aks6d1c6isolem2  42797  unitscyglem5  42821  renegid  42987  sn-0ne2  43020  remul01  43021  remulinvcom  43047  sn-0tie0  43078  renegmulnnass  43092  domnexpgn0cl  43146  abvexp  43155  frlmsnic  43163  fsuppssind  43180  mzpval  43318  mzpindd  43332  pellex  43417  2nn0ind  43527  jm2.26lem3  43583  pw2f1o2val  43621  wepwsolem  43624  fnwe2lem3  43634  lnmfg  43664  dgrsub2  43717  mpaaeu  43732  flcidc  43752  dflim5  43911  naddwordnexlem1  43979  rtrclexlem  44197  cnvrcl0  44206  brcoffn  44611  clsk1indlem3  44624  clsneif1o  44685  clsneicnv  44686  clsneikex  44687  clsneinex  44688  neicvgmex  44698  neicvgel1  44700  suprleubrd  44747  suprlubrd  44749  imo72b2  44753  dvconstbi  44901  bcc0  44907  binomcxplemnotnn0  44923  nnfoctb  45619  infleinflem1  45936  fprodcnlem  46166  sumnnodd  46197  icccncfext  46452  itgsin0pilem1  46515  stoweidlem32  46597  stoweidlem35  46600  stoweidlem36  46601  stoweidlem37  46602  stoweidlem43  46608  stoweidlem50  46615  wallispilem5  46634  stirlinglem2  46640  stirlinglem3  46641  stirlinglem4  46642  stirlinglem8  46646  stirlinglem11  46649  stirlinglem12  46650  stirlinglem14  46652  stirlinglem15  46653  fourierdlem11  46683  fourierdlem20  46692  fourierdlem21  46693  fourierdlem41  46713  fourierdlem42  46714  fourierdlem48  46719  fourierdlem49  46720  fourierdlem64  46735  fourierdlem71  46742  fourierdlem79  46750  fourierdlem90  46761  fourierdlem91  46762  fourierswlem  46795  etransclem17  46816  etransclem38  46837  saluni  46890  meaiininclem  47051  issmflelem  47309  issmfgtlem  47320  issmfgelem  47334  smflimsuplem4  47388  f1cof1blem  47659  zplusmodne  47934  m1modne  47939  submodneaddmod  47942  nndivides2  47969  sprval  48076  prprval  48111  bgoldbtbndlem2  48419  bgoldbtbndlem3  48420  bgoldbtbnd  48422  isubgrvtxuhgr  48477  isubgredg  48479  grimcnv  48501  isuspgrim  48509  gricushgr  48530  uhgrimisgrgric  48544  grtriclwlk3  48558  isubgr3stgrlem7  48585  grlimgrtri  48616  grlictr  48628  gpgvtx0  48666  gpgvtx1  48667  gpgprismgrusgra  48671  gpgedgvtx1  48675  gpg3kgrtriex  48702  pgnbgreunbgrlem3  48731  pgnbgreunbgrlem6  48737  isclintop  48820  clintopcllaw  48824  nzrneg1ne0  48843  lidldomn1  48844  zlidlring  48847  uzlidlring  48848  2zrngnmlid  48868  cznrng  48874  blenre  49187  blennn  49188  2arymaptf  49265  itcoval1  49276  itcovalendof  49282  ehl2eudisval0  49338  eenglngeehlnmlem2  49351  itsclc0yqsol  49377  inlinecirc02plem  49399  ipolub  49600  ipoglb  49603  nelsubclem  49679  imaid  49766  imaf1co  49767  uptri  49826  uptrar  49828  uptrai  49829  oppc1stflem  49899  setrec2mpt  50309