Theorem mpdan 687

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 584	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  689  mpan2  691  biadanid  822  mpjaodan  960  mpjao3dan  1434  mpd3an3  1464  elabd2  3636  eueq2  3681  csbiegf  3895  difsnb  4770  reusv3i  5359  frpoinsg  6316  fimadmfo  6781  fimadmfoALT  6783  fvtresfn  6970  fvmpt3  6972  ffvelcdmd  7057  fnressn  7130  fsnex  7258  f1oiso2  7327  riota5f  7372  onsuc  7787  onsucuni  7803  frrlem10  8274  seqomlem2  8419  oaordi  8510  nnaordi  8582  qsdisj  8767  dom2lem  8963  canth2g  9095  limenpsi  9116  nnfi  9131  php4  9174  onfin  9179  sucxpdom  9202  xpfiOLD  9270  dmfi  9286  fiin  9373  supiso  9427  ordiso2  9468  wdom2d  9533  infeq5  9590  cantnfp1lem3  9633  cantnflem1d  9641  rankwflemb  9746  onenon  9902  cardonle  9910  sdomsdomcardi  9924  acni  9998  cardaleph  10042  djuen  10123  djuinf  10142  infdju1  10143  nnadju  10151  pwsdompw  10156  infdif  10161  cfval  10200  fin34  10343  fin1a2lem1  10353  fin1a2  10368  ttukeylem6  10467  sdomsdomcard  10513  canth3  10514  fpwwe2  10596  canthwelem  10603  gchdju1  10609  pwfseqlem4  10615  gchdjuidm  10621  gchxpidm  10622  tskwe2  10726  rankcf  10730  tskuni  10736  gruxp  10760  dmrecnq  10921  lterpq  10923  archnq  10933  reclem3pr  11002  reclem4pr  11003  0idsr  11050  lep1  12023  ledivp1  12085  negfi  12132  supaddc  12150  supmul1  12152  suprzcl  12614  uz11  12818  zmin  12903  zbtwnre  12905  rpnnen1lem4  12939  rpnnen1lem5  12940  xnegid  13198  supxrre  13287  infxrre  13297  eluzfz2  13493  fzsuc  13532  fzsuc2  13543  fzp1disj  13544  fzneuz  13569  nn0p1elfzo  13663  fllep1  13763  fraclt1  13764  fracle1  13765  fracge0  13766  flhalf  13792  ceige  13806  ceim1l  13809  fldiv  13822  modval  13833  suppssfz  13959  seqeq1  13969  expubnd  14143  iexpcyc  14172  binom2sub1  14186  faclbnd4lem3  14260  pfxid  14649  pfxccatpfx2  14702  swrdccat3blem  14704  cshw0  14759  cshwn  14762  cshimadifsn  14795  cshimadifsn0  14796  pfx2  14913  trclexlem  14960  shftfval  15036  shftcan1  15049  reval  15072  cjmulrcl  15110  addcj  15114  absval  15204  absneg  15243  abscj  15245  sqabsadd  15248  sqabssub  15249  leabs  15265  sqreulem  15326  lo1res  15525  o1of2  15579  o1rlimmul  15585  flo1  15820  trirecip  15829  efcan  16062  efi4p  16105  resin4p  16106  recos4p  16107  sincossq  16144  ruclem10  16207  iddvds  16239  1dvds  16240  2ebits  16417  lcmftp  16606  coprmgcdb  16619  1idssfct  16650  exprmfct  16674  eulerthlem2  16752  odzphi  16767  pcprendvds  16811  pcmpt  16863  oddprmdvds  16874  vdwlem8  16959  0ram2  16992  prmgaplem7  17028  setsn0fun  17143  setsexstruct2  17145  pwsvscaval  17458  2initoinv  17972  initoeu1  17973  initoeu2lem1  17976  initoeu2  17978  2termoinv  17979  termoeu1  17980  homarel  17998  joinfval  18332  meetfval  18346  latjcom  18406  latmcom  18422  0subm  18744  sgrp2nmndlem5  18856  grprcan  18905  isgrpid2  18908  grpinvid  18931  mulgnn0z  19033  0subgOLD  19084  qus0  19121  eqg0subg  19128  ghmker  19174  symgbasmap  19307  symginv  19332  pmtrfrn  19388  odmulg2  19485  slwpgp  19543  pj1eq  19630  efgtf  19652  frgpinv  19694  frgpup2  19706  cnaddablx  19798  cnaddabl  19799  zaddablx  19802  imasabl  19806  dprdfadd  19952  dpjidcl  19990  dpjlid  19993  pgpfac1lem3  20009  srgen1zr  20125  1unit  20283  unitgrpid  20294  1rinv  20304  irredn0  20332  irredneg  20339  c0snmgmhm  20371  rngisomring1  20377  zrrnghm  20445  rnrhmsubrg  20514  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  isdrng2  20652  ringen1zr  20687  abv0  20732  abv1z  20733  abvneg  20735  lmodfopne  20806  lsssn0  20854  lspsn0  20914  lsp0  20915  lmhmvsca  20952  lmhmrnlss  20957  lmhmkerlss  20958  lsppratlem5  21061  rsp1  21147  kerlidl  21188  ring2idlqus  21219  rngqiprngfulem4  21224  rngqiprngfu  21227  cnfldneg  21307  zringcyg  21379  chrid  21435  chrrhm  21441  ip0r  21546  ocvlss  21581  ocv1  21588  rlmassa  21780  psrbagfsupp  21828  snifpsrbag  21829  psrbaglefi  21835  psrvscaval  21859  psrdi  21874  psrdir  21875  mplvscaval  21925  mhpmpl  22031  mhpdeg  22032  mhppwdeg  22037  psdmul  22053  psdpw  22057  coe1sclmulfv  22169  ply1idvr1OLD  22182  evl1var  22223  mamuvs1  22292  mamuvs2  22293  matecl  22312  matvscacell  22323  mat0scmat  22425  submaval0  22467  mdetrsca  22490  maduval  22525  minmar1val0  22534  pmatcollpw3fi1lem2  22674  chcoeffeqlem  22772  cayleyhamilton0  22776  cayleyhamiltonALT  22778  toponsspwpw  22809  cctop  22893  cldval  22910  ntrfval  22911  clsfval  22912  cmclsopn  22949  opncldf3  22973  neifval  22986  lpfval  23025  cnrmnrm  23248  dis2ndc  23347  islocfin  23404  tx1cn  23496  idqtop  23593  kqtopon  23614  kqid  23615  kqcld  23622  hmphen2  23686  filssufil  23799  ufileu  23806  alexsublem  23931  efmndtmd  23988  symgtgp  23993  ustuqtop4  24132  cstucnd  24171  metustexhalf  24444  nm0  24517  rlmnlm  24576  nmolb  24605  metdseq0  24743  pi1xfrval  24954  clmvneg1  24999  clmvsubval  25009  ipcau2  25134  tcphcphlem1  25135  tcphcphlem2  25136  cmetcaulem  25188  ovolicc2lem3  25420  ovolicc2lem4  25421  mbfmulc2lem  25548  i1fpos  25607  mbfi1fseqlem3  25618  itg2ge0  25636  bddiblnc  25743  dvres2  25813  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvfsumlem4  25936  ftc1a  25944  ftc1lem6  25948  uc1pmon1p  26057  ig1pval2  26082  dgradd2  26174  dgrcolem2  26180  plydivlem4  26204  plydiveu  26206  elqaalem3  26229  qaa  26231  ulmdvlem1  26309  abelthlem6  26346  abelthlem7  26348  eflogeq  26511  jensenlem2  26898  harmonicbnd4  26921  sgmnncl  27057  dchrptlem2  27176  1lgs  27251  lgs1  27252  2sqcoprm  27346  addsqnreup  27354  dchrisumlem2  27401  dchrisum0lem2a  27428  selberg2lem  27461  pntrsumo1  27476  pntrsumbnd  27477  pntpbnd1  27497  pntlemr  27513  pntlemj  27514  padicabvf  27542  bdayval  27560  noextendgt  27582  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetainflem4  27652  oldval  27762  divsmul  28123  divscl  28125  seqsp1  28205  zzs12  28339  remulscllem1  28351  incistruhgr  29006  subgrprop3  29203  subgruhgredgd  29211  usgrexi  29368  cusgrexi  29370  cusgrsizeinds  29380  vtxdgfusgrf  29425  1hevtxdg1  29434  1egrvtxdg1  29437  ewlkprop  29531  wlklenvm1  29550  wlkl1loop  29566  wlkp1lem4  29604  2pthnloop  29661  upgrclwlkcompim  29711  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  crctcshlem4  29750  wspthnonp  29789  wlkswwlksf1o  29809  wwlksnwwlksnon  29845  umgr2wlkon  29880  wwlks2onv  29883  elwwlks2ons3im  29884  elwspths2spth  29897  umgrclwwlkge2  29920  clwlkclwwlkf1lem3  29935  erclwwlkref  29949  clwwlknp  29966  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  0pthon1  30057  1wlkdlem4  30069  1pthd  30072  3spthd  30105  eupth2eucrct  30146  eucrctshift  30172  eucrct2eupth  30174  frgrncvvdeqlem8  30235  frgr2wwlkeqm  30260  isgrpoi  30427  grpoinvfval  30451  grpodivfval  30463  vcz  30504  cnaddabloOLD  30510  nvz0  30597  sspz  30664  lno0  30685  nmobndi  30704  ipasslem2  30761  shunssi  31297  ococin  31337  ssjo  31376  pjocini  31627  nlfnval  31810  lncnopbd  31966  riesz3i  31991  cnlnadjlem7  32002  pjclem4  32128  pj3si  32136  hstoc  32151  hstnmoc  32152  hstoh  32161  hst0  32162  mdsl2i  32251  chirredlem3  32321  chirredlem4  32322  dmdbr5ati  32351  rexunirn  32421  fcnvgreu  32597  infxrge0glb  32688  sgnneg  32758  omndmul2  33026  omndmul  33028  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  isarchi3  33141  orng0le1  33290  nsgqusf1olem2  33385  ssdifidllem  33427  ssmxidllem  33444  rprmdvdspow  33504  ressply1sub  33539  fedgmullem1  33625  extdg1id  33661  nn0constr  33751  zartopn  33865  zarcmplem  33871  esumcvg  34076  esumcvgre  34081  sigaval  34101  unelldsys  34148  fiunelros  34164  measval  34188  pmeasmono  34315  probfinmeasb  34419  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsi  34506  ballotlemfrci  34519  signlem0  34578  breprexp  34624  bnj1006  34950  bnj1110  34972  bnj1253  35007  bnj1280  35010  bnj1463  35045  bnj1312  35048  erdszelem7  35184  erdszelem8  35185  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem9  35298  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  satfv1lem  35349  dfrdg2  35783  cldregopn  36319  tailfval  36360  filnetlem3  36368  filnetlem4  36369  ontopbas  36416  bj-elid4  37156  bj-imdiridlem  37173  f1omptsnlem  37324  icoreunrn  37347  relowlpssretop  37352  fvineqsnf1  37398  wl-sbal2  37552  unccur  37597  poimirlem1  37615  poimirlem2  37616  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem17  37631  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem28  37642  poimir  37647  ismblfin  37655  cnambfre  37662  ftc1cnnc  37686  dvasin  37698  ismtyres  37802  heiborlem8  37812  ghomidOLD  37883  rngosn6  37920  rngonegmn1l  37935  rngonegmn1r  37936  rngoneglmul  37937  rngonegrmul  37938  idlnegcl  38016  0idl  38019  0rngo  38021  smprngopr  38046  cossex  38410  qsdisjALTV  38606  cnvepresdmqss  38644  mpets2  38833  lkrval  39081  ldualvaddval  39124  ldualvsval  39131  opoc1  39195  pmap0  39759  pmap1N  39761  pexmidALTN  39972  cdleme31fv  40384  cdlemg27b  40690  erngdvlem4  40985  erng0g  40988  erngdvlem4-rN  40993  dvalveclem  41019  dvh0g  41105  dih0cnv  41277  dih1rn  41281  dih1cnv  41282  doch0  41352  doch1  41353  lcfl7lem  41493  mapdheq  41722  hdmap1eq  41795  hdmapval2lem  41825  hgmapvvlem3  41919  zndvdchrrhm  41960  lcmineqlem13  42029  aks4d1p9  42076  primrootsunit1  42085  aks6d1c1p1  42095  aks6d1c1p6  42102  aks6d1c1p8  42103  sticksstones1  42134  sticksstones6  42139  sticksstones7  42140  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  unitscyglem5  42187  renegid  42361  sn-0ne2  42394  remul01  42395  remulinvcom  42421  sn-0tie0  42439  renegmulnnass  42453  domnexpgn0cl  42511  abvexp  42520  frlmsnic  42528  fsuppssind  42581  mzpval  42720  mzpindd  42734  pellex  42823  2nn0ind  42934  jm2.26lem3  42990  pw2f1o2val  43028  wepwsolem  43031  fnwe2lem3  43041  lnmfg  43071  dgrsub2  43124  mpaaeu  43139  flcidc  43159  dflim5  43318  naddwordnexlem1  43386  rtrclexlem  43605  cnvrcl0  43614  brcoffn  44019  clsk1indlem3  44032  clsneif1o  44093  clsneicnv  44094  clsneikex  44095  clsneinex  44096  neicvgmex  44106  neicvgel1  44108  suprleubrd  44155  suprlubrd  44157  imo72b2  44161  dvconstbi  44323  bcc0  44329  binomcxplemnotnn0  44345  nnfoctb  45042  infleinflem1  45366  fprodcnlem  45597  sumnnodd  45628  icccncfext  45885  itgsin0pilem1  45948  stoweidlem32  46030  stoweidlem35  46033  stoweidlem36  46034  stoweidlem37  46035  stoweidlem43  46041  stoweidlem50  46048  wallispilem5  46067  stirlinglem2  46073  stirlinglem3  46074  stirlinglem4  46075  stirlinglem8  46079  stirlinglem11  46082  stirlinglem12  46083  stirlinglem14  46085  stirlinglem15  46086  fourierdlem11  46116  fourierdlem20  46125  fourierdlem21  46126  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem64  46168  fourierdlem71  46175  fourierdlem79  46183  fourierdlem90  46194  fourierdlem91  46195  fourierswlem  46228  etransclem17  46249  etransclem38  46270  saluni  46323  meaiininclem  46484  issmflelem  46742  issmfgtlem  46753  issmfgelem  46767  smflimsuplem4  46821  f1cof1blem  47075  zplusmodne  47344  m1modne  47349  submodneaddmod  47352  sprval  47480  prprval  47515  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  isubgrvtxuhgr  47864  isubgredg  47866  grimcnv  47888  isuspgrim  47896  gricushgr  47917  uhgrimisgrgric  47931  grtriclwlk3  47944  isubgr3stgrlem7  47971  grlimgrtri  47995  grlictr  48007  gpgvtx0  48044  gpgvtx1  48045  gpgprismgrusgra  48049  gpgedgvtx1  48053  gpg3kgrtriex  48080  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  isclintop  48195  clintopcllaw  48199  nzrneg1ne0  48218  lidldomn1  48219  zlidlring  48222  uzlidlring  48223  2zrngnmlid  48243  cznrng  48249  coe1id  48373  blenre  48563  blennn  48564  2arymaptf  48641  itcoval1  48652  itcovalendof  48658  ehl2eudisval0  48714  eenglngeehlnmlem2  48727  itsclc0yqsol  48753  inlinecirc02plem  48775  ipolub  48976  ipoglb  48979  nelsubclem  49056  imaid  49143  imaf1co  49144  uptri  49203  uptrar  49205  uptrai  49206  oppc1stflem  49276  setrec2mpt  49686