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  3625  eueq2  3669  csbiegf  3883  difsnb  4763  reusv3i  5350  frpoinsg  6302  fimadmfo  6756  fimadmfoALT  6758  fvtresfn  6945  fvmpt3  6947  ffvelcdmd  7032  fnressn  7105  fsnex  7231  f1oiso2  7300  riota5f  7345  onsuc  7757  onsucuni  7772  frrlem10  8239  seqomlem2  8384  oaordi  8475  nnaordi  8548  qsdisj  8735  dom2lem  8933  canth2g  9063  limenpsi  9084  nnfi  9096  php4  9138  onfin  9143  sucxpdom  9165  dmfi  9239  fiin  9329  supiso  9383  ordiso2  9424  wdom2d  9489  elirrv  9506  infeq5  9550  cantnfp1lem3  9593  cantnflem1d  9601  rankwflemb  9709  onenon  9865  cardonle  9873  sdomsdomcardi  9887  acni  9959  cardaleph  10003  djuen  10084  djuinf  10103  infdju1  10104  nnadju  10112  pwsdompw  10117  infdif  10122  cfval  10161  fin34  10304  fin1a2lem1  10314  fin1a2  10329  ttukeylem6  10428  sdomsdomcard  10474  canth3  10475  fpwwe2  10558  canthwelem  10565  gchdju1  10571  pwfseqlem4  10577  gchdjuidm  10583  gchxpidm  10584  tskwe2  10688  rankcf  10692  tskuni  10698  gruxp  10722  dmrecnq  10883  lterpq  10885  archnq  10895  reclem3pr  10964  reclem4pr  10965  0idsr  11012  lep1  11986  ledivp1  12048  negfi  12095  supaddc  12113  supmul1  12115  suprzcl  12576  uz11  12780  zmin  12861  zbtwnre  12863  rpnnen1lem4  12897  rpnnen1lem5  12898  xnegid  13157  supxrre  13246  infxrre  13256  eluzfz2  13452  fzsuc  13491  fzsuc2  13502  fzp1disj  13503  fzneuz  13528  nn0p1elfzo  13622  fllep1  13725  fraclt1  13726  fracle1  13727  fracge0  13728  flhalf  13754  ceige  13768  ceim1l  13771  fldiv  13784  modval  13795  suppssfz  13921  seqeq1  13931  expubnd  14105  iexpcyc  14134  binom2sub1  14148  faclbnd4lem3  14222  pfxid  14612  pfxccatpfx2  14664  swrdccat3blem  14666  cshw0  14721  cshwn  14724  cshimadifsn  14756  cshimadifsn0  14757  pfx2  14874  trclexlem  14921  shftfval  14997  shftcan1  15010  reval  15033  cjmulrcl  15071  addcj  15075  absval  15165  absneg  15204  abscj  15206  sqabsadd  15209  sqabssub  15210  leabs  15226  sqreulem  15287  lo1res  15486  o1of2  15540  o1rlimmul  15546  flo1  15781  trirecip  15790  efcan  16023  efi4p  16066  resin4p  16067  recos4p  16068  sincossq  16105  ruclem10  16168  iddvds  16200  1dvds  16201  2ebits  16378  lcmftp  16567  coprmgcdb  16580  1idssfct  16611  exprmfct  16635  eulerthlem2  16713  odzphi  16728  pcprendvds  16772  pcmpt  16824  oddprmdvds  16835  vdwlem8  16920  0ram2  16953  prmgaplem7  16989  setsn0fun  17104  setsexstruct2  17106  pwsvscaval  17420  2initoinv  17938  initoeu1  17939  initoeu2lem1  17942  initoeu2  17944  2termoinv  17945  termoeu1  17946  homarel  17964  joinfval  18298  meetfval  18312  latjcom  18374  latmcom  18390  0subm  18746  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  20314  unitgrpid  20325  1rinv  20335  irredn0  20363  irredneg  20370  c0snmgmhm  20402  rngisomring1  20408  zrrnghm  20473  rnrhmsubrg  20542  zrinitorngc  20579  zrtermorngc  20580  zrtermoringc  20612  isdrng2  20680  ringen1zr  20715  abv0  20760  abv1z  20761  abvneg  20763  orng0le1  20811  lmodfopne  20855  lsssn0  20903  lspsn0  20963  lsp0  20964  lmhmvsca  21001  lmhmrnlss  21006  lmhmkerlss  21007  lsppratlem5  21110  rsp1  21196  kerlidl  21237  ring2idlqus  21268  rngqiprngfulem4  21273  rngqiprngfu  21276  cnfldneg  21354  zringcyg  21428  chrid  21484  chrrhm  21490  ip0r  21596  ocvlss  21631  ocv1  21638  rlmassa  21830  psrbagfsupp  21879  snifpsrbag  21880  psrbaglefi  21886  psrvscaval  21910  psrdi  21924  psrdir  21925  mplvscaval  21975  mhpmpl  22091  mhpdeg  22092  mhppwdeg  22097  psdmul  22113  psdpw  22117  coe1sclmulfv  22229  coe1id  22241  ply1idvr1OLD  22243  evl1var  22284  mamuvs1  22353  mamuvs2  22354  matecl  22373  matvscacell  22384  mat0scmat  22486  submaval0  22528  mdetrsca  22551  maduval  22586  minmar1val0  22595  pmatcollpw3fi1lem2  22735  chcoeffeqlem  22833  cayleyhamilton0  22837  cayleyhamiltonALT  22839  toponsspwpw  22870  cctop  22954  cldval  22971  ntrfval  22972  clsfval  22973  cmclsopn  23010  opncldf3  23034  neifval  23047  lpfval  23086  cnrmnrm  23309  dis2ndc  23408  islocfin  23465  tx1cn  23557  idqtop  23654  kqtopon  23675  kqid  23676  kqcld  23683  hmphen2  23747  filssufil  23860  ufileu  23867  alexsublem  23992  efmndtmd  24049  symgtgp  24054  ustuqtop4  24192  cstucnd  24231  metustexhalf  24504  nm0  24577  rlmnlm  24636  nmolb  24665  metdseq0  24803  pi1xfrval  25014  clmvneg1  25059  clmvsubval  25069  ipcau2  25194  tcphcphlem1  25195  tcphcphlem2  25196  cmetcaulem  25248  ovolicc2lem3  25480  ovolicc2lem4  25481  mbfmulc2lem  25608  i1fpos  25667  mbfi1fseqlem3  25678  itg2ge0  25696  bddiblnc  25803  dvres2  25873  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcobr  25909  dvcobrOLD  25910  dvfsumlem4  25996  ftc1a  26004  ftc1lem6  26008  uc1pmon1p  26117  ig1pval2  26142  dgradd2  26234  dgrcolem2  26240  plydivlem4  26264  plydiveu  26266  elqaalem3  26289  qaa  26291  ulmdvlem1  26369  abelthlem6  26406  abelthlem7  26408  eflogeq  26571  jensenlem2  26958  harmonicbnd4  26981  sgmnncl  27117  dchrptlem2  27236  1lgs  27311  lgs1  27312  2sqcoprm  27406  addsqnreup  27414  dchrisumlem2  27461  dchrisum0lem2a  27488  selberg2lem  27521  pntrsumo1  27536  pntrsumbnd  27537  pntpbnd1  27557  pntlemr  27573  pntlemj  27574  padicabvf  27602  bdayval  27620  noextendgt  27642  nosupbnd2lem1  27687  noinfbnd2lem1  27702  noetainflem4  27712  oldval  27832  divsmul  28202  divscl  28204  seqsp1  28292  zzs12  28454  remulscllem1  28479  incistruhgr  29135  subgrprop3  29332  subgruhgredgd  29340  usgrexi  29497  cusgrexi  29499  cusgrsizeinds  29509  vtxdgfusgrf  29554  1hevtxdg1  29563  1egrvtxdg1  29566  ewlkprop  29660  wlklenvm1  29678  wlkl1loop  29694  wlkp1lem4  29731  2pthnloop  29787  upgrclwlkcompim  29837  crctcshwlkn0lem4  29869  crctcshwlkn0lem5  29870  crctcshwlkn0lem6  29871  crctcshwlkn0lem7  29872  crctcshlem4  29876  wspthnonp  29915  wlkswwlksf1o  29935  wwlksnwwlksnon  29971  umgr2wlkon  30006  wwlks2onv  30009  elwwlks2ons3im  30010  elwspths2spth  30026  umgrclwwlkge2  30049  clwlkclwwlkf1lem3  30064  erclwwlkref  30078  clwwlknp  30095  wwlksext2clwwlk  30115  wwlksubclwwlk  30116  0pthon1  30186  1wlkdlem4  30198  1pthd  30201  3spthd  30234  eupth2eucrct  30275  eucrctshift  30301  eucrct2eupth  30303  frgrncvvdeqlem8  30364  frgr2wwlkeqm  30389  isgrpoi  30556  grpoinvfval  30580  grpodivfval  30592  vcz  30633  cnaddabloOLD  30639  nvz0  30726  sspz  30793  lno0  30814  nmobndi  30833  ipasslem2  30890  shunssi  31426  ococin  31466  ssjo  31505  pjocini  31756  nlfnval  31939  lncnopbd  32095  riesz3i  32120  cnlnadjlem7  32131  pjclem4  32257  pj3si  32265  hstoc  32280  hstnmoc  32281  hstoh  32290  hst0  32291  mdsl2i  32380  chirredlem3  32450  chirredlem4  32451  dmdbr5ati  32480  rexunirn  32548  fcnvgreu  32732  infxrge0glb  32826  sgnneg  32895  cycpmco2lem5  33193  cycpmco2lem6  33194  cycpmco2lem7  33195  isarchi3  33250  nsgqusf1olem2  33476  ssdifidllem  33518  ssmxidllem  33535  rprmdvdspow  33595  ressply1sub  33632  fedgmullem1  33767  extdg1id  33804  nn0constr  33899  zartopn  34013  zarcmplem  34019  esumcvg  34224  esumcvgre  34229  sigaval  34249  unelldsys  34296  fiunelros  34312  measval  34336  pmeasmono  34462  probfinmeasb  34566  ballotlemfc0  34631  ballotlemfcc  34632  ballotlemsi  34653  ballotlemfrci  34666  signlem0  34725  breprexp  34771  bnj1006  35097  bnj1110  35119  bnj1253  35154  bnj1280  35157  bnj1463  35192  bnj1312  35195  fineqvinfep  35262  erdszelem7  35372  erdszelem8  35373  cvmliftlem10  35469  cvmliftlem13  35471  cvmlift2lem9  35486  cvmlift3lem6  35499  cvmlift3lem7  35500  cvmlift3lem9  35502  satfv1lem  35537  dfrdg2  35968  cldregopn  36506  tailfval  36547  filnetlem3  36555  filnetlem4  36556  ontopbas  36603  bj-elid4  37344  bj-imdiridlem  37361  f1omptsnlem  37512  icoreunrn  37535  relowlpssretop  37540  fvineqsnf1  37586  wl-sbal2  37740  unccur  37775  poimirlem1  37793  poimirlem2  37794  poimirlem4  37796  poimirlem6  37798  poimirlem7  37799  poimirlem11  37803  poimirlem12  37804  poimirlem17  37809  poimirlem20  37812  poimirlem22  37814  poimirlem23  37815  poimirlem28  37820  poimir  37825  ismblfin  37833  cnambfre  37840  ftc1cnnc  37864  dvasin  37876  ismtyres  37980  heiborlem8  37990  ghomidOLD  38061  rngosn6  38098  rngonegmn1l  38113  rngonegmn1r  38114  rngoneglmul  38115  rngonegrmul  38116  idlnegcl  38194  0idl  38197  0rngo  38199  smprngopr  38224  sucmapsuc  38661  cossex  38681  qsdisjALTV  38871  cnvepresdmqss  38909  mpets2  39127  lkrval  39385  ldualvaddval  39428  ldualvsval  39435  opoc1  39499  pmap0  40062  pmap1N  40064  pexmidALTN  40275  cdleme31fv  40687  cdlemg27b  40993  erngdvlem4  41288  erng0g  41291  erngdvlem4-rN  41296  dvalveclem  41322  dvh0g  41408  dih0cnv  41580  dih1rn  41584  dih1cnv  41585  doch0  41655  doch1  41656  lcfl7lem  41796  mapdheq  42025  hdmap1eq  42098  hdmapval2lem  42128  hgmapvvlem3  42222  zndvdchrrhm  42263  lcmineqlem13  42332  aks4d1p9  42379  primrootsunit1  42388  aks6d1c1p1  42398  aks6d1c1p6  42405  aks6d1c1p8  42406  sticksstones1  42437  sticksstones6  42442  sticksstones7  42443  sticksstones11  42447  sticksstones12a  42448  sticksstones12  42449  sticksstones22  42459  aks6d1c6isolem1  42465  aks6d1c6isolem2  42466  unitscyglem5  42490  renegid  42664  sn-0ne2  42697  remul01  42698  remulinvcom  42724  sn-0tie0  42742  renegmulnnass  42756  domnexpgn0cl  42814  abvexp  42823  frlmsnic  42831  fsuppssind  42872  mzpval  43010  mzpindd  43024  pellex  43113  2nn0ind  43223  jm2.26lem3  43279  pw2f1o2val  43317  wepwsolem  43320  fnwe2lem3  43330  lnmfg  43360  dgrsub2  43413  mpaaeu  43428  flcidc  43448  dflim5  43607  naddwordnexlem1  43675  rtrclexlem  43893  cnvrcl0  43902  brcoffn  44307  clsk1indlem3  44320  clsneif1o  44381  clsneicnv  44382  clsneikex  44383  clsneinex  44384  neicvgmex  44394  neicvgel1  44396  suprleubrd  44443  suprlubrd  44445  imo72b2  44449  dvconstbi  44611  bcc0  44617  binomcxplemnotnn0  44633  nnfoctb  45329  infleinflem1  45650  fprodcnlem  45881  sumnnodd  45912  icccncfext  46167  itgsin0pilem1  46230  stoweidlem32  46312  stoweidlem35  46315  stoweidlem36  46316  stoweidlem37  46317  stoweidlem43  46323  stoweidlem50  46330  wallispilem5  46349  stirlinglem2  46355  stirlinglem3  46356  stirlinglem4  46357  stirlinglem8  46361  stirlinglem11  46364  stirlinglem12  46365  stirlinglem14  46367  stirlinglem15  46368  fourierdlem11  46398  fourierdlem20  46407  fourierdlem21  46408  fourierdlem41  46428  fourierdlem42  46429  fourierdlem48  46434  fourierdlem49  46435  fourierdlem64  46450  fourierdlem71  46457  fourierdlem79  46465  fourierdlem90  46476  fourierdlem91  46477  fourierswlem  46510  etransclem17  46531  etransclem38  46552  saluni  46605  meaiininclem  46766  issmflelem  47024  issmfgtlem  47035  issmfgelem  47049  smflimsuplem4  47103  f1cof1blem  47356  zplusmodne  47625  m1modne  47630  submodneaddmod  47633  sprval  47761  prprval  47796  bgoldbtbndlem2  48088  bgoldbtbndlem3  48089  bgoldbtbnd  48091  isubgrvtxuhgr  48146  isubgredg  48148  grimcnv  48170  isuspgrim  48178  gricushgr  48199  uhgrimisgrgric  48213  grtriclwlk3  48227  isubgr3stgrlem7  48254  grlimgrtri  48285  grlictr  48297  gpgvtx0  48335  gpgvtx1  48336  gpgprismgrusgra  48340  gpgedgvtx1  48344  gpg3kgrtriex  48371  pgnbgreunbgrlem3  48400  pgnbgreunbgrlem6  48406  isclintop  48489  clintopcllaw  48493  nzrneg1ne0  48512  lidldomn1  48513  zlidlring  48516  uzlidlring  48517  2zrngnmlid  48537  cznrng  48543  blenre  48856  blennn  48857  2arymaptf  48934  itcoval1  48945  itcovalendof  48951  ehl2eudisval0  49007  eenglngeehlnmlem2  49020  itsclc0yqsol  49046  inlinecirc02plem  49068  ipolub  49269  ipoglb  49272  nelsubclem  49348  imaid  49435  imaf1co  49436  uptri  49495  uptrar  49497  uptrai  49498  oppc1stflem  49568  setrec2mpt  49978