Theorem mpdan 688

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 585	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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-an 396

This theorem is referenced by:  mpidan  690  mpan2  692  biadanid  823  mpjaodan  961  mpjao3dan  1435  mpd3an3  1465  elabd2  3613  eueq2  3657  csbiegf  3871  difsnb  4750  reusv3i  5339  frpoinsg  6299  fimadmfo  6753  fimadmfoALT  6755  fvtresfn  6942  fvmpt3  6944  ffvelcdmd  7029  fnressn  7103  fsnex  7229  f1oiso2  7298  riota5f  7343  onsuc  7755  onsucuni  7770  frrlem10  8236  seqomlem2  8381  oaordi  8472  nnaordi  8545  qsdisj  8732  dom2lem  8930  canth2g  9060  limenpsi  9081  nnfi  9093  php4  9135  onfin  9140  sucxpdom  9162  dmfi  9236  fiin  9326  supiso  9380  ordiso2  9421  wdom2d  9486  elirrv  9503  infeq5  9547  cantnfp1lem3  9590  cantnflem1d  9598  rankwflemb  9706  onenon  9862  cardonle  9870  sdomsdomcardi  9884  acni  9956  cardaleph  10000  djuen  10081  djuinf  10100  infdju1  10101  nnadju  10109  pwsdompw  10114  infdif  10119  cfval  10158  fin34  10301  fin1a2lem1  10311  fin1a2  10326  ttukeylem6  10425  sdomsdomcard  10471  canth3  10472  fpwwe2  10555  canthwelem  10562  gchdju1  10568  pwfseqlem4  10574  gchdjuidm  10580  gchxpidm  10581  tskwe2  10685  rankcf  10689  tskuni  10695  gruxp  10719  dmrecnq  10880  lterpq  10882  archnq  10892  reclem3pr  10961  reclem4pr  10962  0idsr  11009  lep1  11983  ledivp1  12045  negfi  12092  supaddc  12110  supmul1  12112  suprzcl  12573  uz11  12777  zmin  12858  zbtwnre  12860  rpnnen1lem4  12894  rpnnen1lem5  12895  xnegid  13154  supxrre  13243  infxrre  13253  eluzfz2  13449  fzsuc  13488  fzsuc2  13499  fzp1disj  13500  fzneuz  13525  nn0p1elfzo  13619  fllep1  13722  fraclt1  13723  fracle1  13724  fracge0  13725  flhalf  13751  ceige  13765  ceim1l  13768  fldiv  13781  modval  13792  suppssfz  13918  seqeq1  13928  expubnd  14102  iexpcyc  14131  binom2sub1  14145  faclbnd4lem3  14219  pfxid  14609  pfxccatpfx2  14661  swrdccat3blem  14663  cshw0  14718  cshwn  14721  cshimadifsn  14753  cshimadifsn0  14754  pfx2  14871  trclexlem  14918  shftfval  14994  shftcan1  15007  reval  15030  cjmulrcl  15068  addcj  15072  absval  15162  absneg  15201  abscj  15203  sqabsadd  15206  sqabssub  15207  leabs  15223  sqreulem  15284  lo1res  15483  o1of2  15537  o1rlimmul  15543  flo1  15778  trirecip  15787  efcan  16020  efi4p  16063  resin4p  16064  recos4p  16065  sincossq  16102  ruclem10  16165  iddvds  16197  1dvds  16198  2ebits  16375  lcmftp  16564  coprmgcdb  16577  1idssfct  16608  exprmfct  16632  eulerthlem2  16710  odzphi  16725  pcprendvds  16769  pcmpt  16821  oddprmdvds  16832  vdwlem8  16917  0ram2  16950  prmgaplem7  16986  setsn0fun  17101  setsexstruct2  17103  pwsvscaval  17417  2initoinv  17935  initoeu1  17936  initoeu2lem1  17939  initoeu2  17941  2termoinv  17942  termoeu1  17943  homarel  17961  joinfval  18295  meetfval  18309  latjcom  18371  latmcom  18387  0subm  18743  sgrp2nmndlem5  18858  grprcan  18907  isgrpid2  18910  grpinvid  18933  mulgnn0z  19035  qus0  19122  eqg0subg  19129  ghmker  19175  symgbasmap  19310  symginv  19335  pmtrfrn  19391  odmulg2  19488  slwpgp  19546  pj1eq  19633  efgtf  19655  frgpinv  19697  frgpup2  19709  cnaddablx  19801  cnaddabl  19802  zaddablx  19805  imasabl  19809  dprdfadd  19955  dpjidcl  19993  dpjlid  19996  pgpfac1lem3  20012  omndmul2  20066  omndmul  20068  srgen1zr  20155  1unit  20312  unitgrpid  20323  1rinv  20333  irredn0  20361  irredneg  20368  c0snmgmhm  20400  rngisomring1  20406  zrrnghm  20471  rnrhmsubrg  20540  zrinitorngc  20577  zrtermorngc  20578  zrtermoringc  20610  isdrng2  20678  ringen1zr  20713  abv0  20758  abv1z  20759  abvneg  20761  orng0le1  20809  lmodfopne  20853  lsssn0  20901  lspsn0  20961  lsp0  20962  lmhmvsca  20999  lmhmrnlss  21004  lmhmkerlss  21005  lsppratlem5  21108  rsp1  21194  kerlidl  21235  ring2idlqus  21266  rngqiprngfulem4  21271  rngqiprngfu  21274  cnfldneg  21352  zringcyg  21426  chrid  21482  chrrhm  21488  ip0r  21594  ocvlss  21629  ocv1  21636  rlmassa  21827  psrbagfsupp  21876  snifpsrbag  21877  psrbaglefi  21883  psrvscaval  21907  psrdi  21921  psrdir  21922  mplvscaval  21972  mhpmpl  22088  mhpdeg  22089  mhppwdeg  22094  psdmul  22110  psdpw  22114  coe1sclmulfv  22226  coe1id  22236  ply1idvr1OLD  22238  evl1var  22279  mamuvs1  22348  mamuvs2  22349  matecl  22368  matvscacell  22379  mat0scmat  22481  submaval0  22523  mdetrsca  22546  maduval  22581  minmar1val0  22590  pmatcollpw3fi1lem2  22730  chcoeffeqlem  22828  cayleyhamilton0  22832  cayleyhamiltonALT  22834  toponsspwpw  22865  cctop  22949  cldval  22966  ntrfval  22967  clsfval  22968  cmclsopn  23005  opncldf3  23029  neifval  23042  lpfval  23081  cnrmnrm  23304  dis2ndc  23403  islocfin  23460  tx1cn  23552  idqtop  23649  kqtopon  23670  kqid  23671  kqcld  23678  hmphen2  23742  filssufil  23855  ufileu  23862  alexsublem  23987  efmndtmd  24044  symgtgp  24049  ustuqtop4  24187  cstucnd  24226  metustexhalf  24499  nm0  24572  rlmnlm  24631  nmolb  24660  metdseq0  24798  pi1xfrval  24999  clmvneg1  25044  clmvsubval  25054  ipcau2  25179  tcphcphlem1  25180  tcphcphlem2  25181  cmetcaulem  25233  ovolicc2lem3  25464  ovolicc2lem4  25465  mbfmulc2lem  25592  i1fpos  25651  mbfi1fseqlem3  25662  itg2ge0  25680  bddiblnc  25787  dvres2  25857  dvaddbr  25883  dvmulbr  25884  dvcobr  25891  dvfsumlem4  25977  ftc1a  25985  ftc1lem6  25989  uc1pmon1p  26098  ig1pval2  26123  dgradd2  26214  dgrcolem2  26220  plydivlem4  26244  plydiveu  26246  elqaalem3  26269  qaa  26271  ulmdvlem1  26349  abelthlem6  26386  abelthlem7  26388  eflogeq  26551  jensenlem2  26938  harmonicbnd4  26961  sgmnncl  27097  dchrptlem2  27216  1lgs  27291  lgs1  27292  2sqcoprm  27386  addsqnreup  27394  dchrisumlem2  27441  dchrisum0lem2a  27468  selberg2lem  27501  pntrsumo1  27516  pntrsumbnd  27517  pntpbnd1  27537  pntlemr  27553  pntlemj  27554  padicabvf  27582  bdayval  27600  noextendgt  27622  nosupbnd2lem1  27667  noinfbnd2lem1  27682  noetainflem4  27692  oldval  27814  divmuls  28201  divscl  28203  seqsp1  28291  bdayfinbndlem1  28447  zz12s  28455  remulscllem1  28480  incistruhgr  29136  subgrprop3  29333  subgruhgredgd  29341  usgrexi  29498  cusgrexi  29500  cusgrsizeinds  29510  vtxdgfusgrf  29555  1hevtxdg1  29564  1egrvtxdg1  29567  ewlkprop  29661  wlklenvm1  29679  wlkl1loop  29695  wlkp1lem4  29732  2pthnloop  29788  upgrclwlkcompim  29838  crctcshwlkn0lem4  29870  crctcshwlkn0lem5  29871  crctcshwlkn0lem6  29872  crctcshwlkn0lem7  29873  crctcshlem4  29877  wspthnonp  29916  wlkswwlksf1o  29936  wwlksnwwlksnon  29972  umgr2wlkon  30007  wwlks2onv  30010  elwwlks2ons3im  30011  elwspths2spth  30027  umgrclwwlkge2  30050  clwlkclwwlkf1lem3  30065  erclwwlkref  30079  clwwlknp  30096  wwlksext2clwwlk  30116  wwlksubclwwlk  30117  0pthon1  30187  1wlkdlem4  30199  1pthd  30202  3spthd  30235  eupth2eucrct  30276  eucrctshift  30302  eucrct2eupth  30304  frgrncvvdeqlem8  30365  frgr2wwlkeqm  30390  isgrpoi  30558  grpoinvfval  30582  grpodivfval  30594  vcz  30635  cnaddabloOLD  30641  nvz0  30728  sspz  30795  lno0  30816  nmobndi  30835  ipasslem2  30892  shunssi  31428  ococin  31468  ssjo  31507  pjocini  31758  nlfnval  31941  lncnopbd  32097  riesz3i  32122  cnlnadjlem7  32133  pjclem4  32259  pj3si  32267  hstoc  32282  hstnmoc  32283  hstoh  32292  hst0  32293  mdsl2i  32382  chirredlem3  32452  chirredlem4  32453  dmdbr5ati  32482  rexunirn  32550  fcnvgreu  32734  infxrge0glb  32828  sgnneg  32897  cycpmco2lem5  33196  cycpmco2lem6  33197  cycpmco2lem7  33198  isarchi3  33253  nsgqusf1olem2  33479  ssdifidllem  33521  ssmxidllem  33538  rprmdvdspow  33598  ressply1sub  33635  fedgmullem1  33779  extdg1id  33816  nn0constr  33911  zartopn  34025  zarcmplem  34031  esumcvg  34236  esumcvgre  34241  sigaval  34261  unelldsys  34308  fiunelros  34324  measval  34348  pmeasmono  34474  probfinmeasb  34578  ballotlemfc0  34643  ballotlemfcc  34644  ballotlemsi  34665  ballotlemfrci  34678  signlem0  34737  breprexp  34783  bnj1006  35108  bnj1110  35130  bnj1253  35165  bnj1280  35168  bnj1463  35203  bnj1312  35206  fineqvinfep  35275  erdszelem7  35385  erdszelem8  35386  cvmliftlem10  35482  cvmliftlem13  35484  cvmlift2lem9  35499  cvmlift3lem6  35512  cvmlift3lem7  35513  cvmlift3lem9  35515  satfv1lem  35550  dfrdg2  35981  cldregopn  36519  tailfval  36560  filnetlem3  36568  filnetlem4  36569  ontopbas  36616  bj-nnfbd  37064  bj-elid4  37480  bj-imdiridlem  37497  f1omptsnlem  37648  icoreunrn  37671  relowlpssretop  37676  fvineqsnf1  37722  wl-sbal2  37880  unccur  37915  poimirlem1  37933  poimirlem2  37934  poimirlem4  37936  poimirlem6  37938  poimirlem7  37939  poimirlem11  37943  poimirlem12  37944  poimirlem17  37949  poimirlem20  37952  poimirlem22  37954  poimirlem23  37955  poimirlem28  37960  poimir  37965  ismblfin  37973  cnambfre  37980  ftc1cnnc  38004  dvasin  38016  ismtyres  38120  heiborlem8  38130  ghomidOLD  38201  rngosn6  38238  rngonegmn1l  38253  rngonegmn1r  38254  rngoneglmul  38255  rngonegrmul  38256  idlnegcl  38334  0idl  38337  0rngo  38339  smprngopr  38364  sucmapsuc  38801  cossex  38821  qsdisjALTV  39011  cnvepresdmqss  39049  mpets2  39267  lkrval  39525  ldualvaddval  39568  ldualvsval  39575  opoc1  39639  pmap0  40202  pmap1N  40204  pexmidALTN  40415  cdleme31fv  40827  cdlemg27b  41133  erngdvlem4  41428  erng0g  41431  erngdvlem4-rN  41436  dvalveclem  41462  dvh0g  41548  dih0cnv  41720  dih1rn  41724  dih1cnv  41725  doch0  41795  doch1  41796  lcfl7lem  41936  mapdheq  42165  hdmap1eq  42238  hdmapval2lem  42268  hgmapvvlem3  42362  zndvdchrrhm  42403  lcmineqlem13  42472  aks4d1p9  42519  primrootsunit1  42528  aks6d1c1p1  42538  aks6d1c1p6  42545  aks6d1c1p8  42546  sticksstones1  42577  sticksstones6  42582  sticksstones7  42583  sticksstones11  42587  sticksstones12a  42588  sticksstones12  42589  sticksstones22  42599  aks6d1c6isolem1  42605  aks6d1c6isolem2  42606  unitscyglem5  42630  renegid  42804  sn-0ne2  42837  remul01  42838  remulinvcom  42864  sn-0tie0  42895  renegmulnnass  42909  domnexpgn0cl  42967  abvexp  42976  frlmsnic  42984  fsuppssind  43025  mzpval  43163  mzpindd  43177  pellex  43266  2nn0ind  43376  jm2.26lem3  43432  pw2f1o2val  43470  wepwsolem  43473  fnwe2lem3  43483  lnmfg  43513  dgrsub2  43566  mpaaeu  43581  flcidc  43601  dflim5  43760  naddwordnexlem1  43828  rtrclexlem  44046  cnvrcl0  44055  brcoffn  44460  clsk1indlem3  44473  clsneif1o  44534  clsneicnv  44535  clsneikex  44536  clsneinex  44537  neicvgmex  44547  neicvgel1  44549  suprleubrd  44596  suprlubrd  44598  imo72b2  44602  dvconstbi  44764  bcc0  44770  binomcxplemnotnn0  44786  nnfoctb  45482  infleinflem1  45802  fprodcnlem  46033  sumnnodd  46064  icccncfext  46319  itgsin0pilem1  46382  stoweidlem32  46464  stoweidlem35  46467  stoweidlem36  46468  stoweidlem37  46469  stoweidlem43  46475  stoweidlem50  46482  wallispilem5  46501  stirlinglem2  46507  stirlinglem3  46508  stirlinglem4  46509  stirlinglem8  46513  stirlinglem11  46516  stirlinglem12  46517  stirlinglem14  46519  stirlinglem15  46520  fourierdlem11  46550  fourierdlem20  46559  fourierdlem21  46560  fourierdlem41  46580  fourierdlem42  46581  fourierdlem48  46586  fourierdlem49  46587  fourierdlem64  46602  fourierdlem71  46609  fourierdlem79  46617  fourierdlem90  46628  fourierdlem91  46629  fourierswlem  46662  etransclem17  46683  etransclem38  46704  saluni  46757  meaiininclem  46918  issmflelem  47176  issmfgtlem  47187  issmfgelem  47201  smflimsuplem4  47255  f1cof1blem  47508  zplusmodne  47777  m1modne  47782  submodneaddmod  47785  sprval  47913  prprval  47948  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  bgoldbtbnd  48243  isubgrvtxuhgr  48298  isubgredg  48300  grimcnv  48322  isuspgrim  48330  gricushgr  48351  uhgrimisgrgric  48365  grtriclwlk3  48379  isubgr3stgrlem7  48406  grlimgrtri  48437  grlictr  48449  gpgvtx0  48487  gpgvtx1  48488  gpgprismgrusgra  48492  gpgedgvtx1  48496  gpg3kgrtriex  48523  pgnbgreunbgrlem3  48552  pgnbgreunbgrlem6  48558  isclintop  48641  clintopcllaw  48645  nzrneg1ne0  48664  lidldomn1  48665  zlidlring  48668  uzlidlring  48669  2zrngnmlid  48689  cznrng  48695  blenre  49008  blennn  49009  2arymaptf  49086  itcoval1  49097  itcovalendof  49103  ehl2eudisval0  49159  eenglngeehlnmlem2  49172  itsclc0yqsol  49198  inlinecirc02plem  49220  ipolub  49421  ipoglb  49424  nelsubclem  49500  imaid  49587  imaf1co  49588  uptri  49647  uptrar  49649  uptrai  49650  oppc1stflem  49720  setrec2mpt  50130