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  7106  fsnex  7232  f1oiso2  7301  riota5f  7346  onsuc  7758  onsucuni  7773  frrlem10  8240  seqomlem2  8385  oaordi  8476  nnaordi  8549  qsdisj  8736  dom2lem  8934  canth2g  9064  limenpsi  9085  nnfi  9097  php4  9139  onfin  9144  sucxpdom  9166  dmfi  9240  fiin  9330  supiso  9384  ordiso2  9425  wdom2d  9490  elirrv  9507  infeq5  9551  cantnfp1lem3  9594  cantnflem1d  9602  rankwflemb  9710  onenon  9866  cardonle  9874  sdomsdomcardi  9888  acni  9960  cardaleph  10004  djuen  10085  djuinf  10104  infdju1  10105  nnadju  10113  pwsdompw  10118  infdif  10123  cfval  10162  fin34  10305  fin1a2lem1  10315  fin1a2  10330  ttukeylem6  10429  sdomsdomcard  10475  canth3  10476  fpwwe2  10559  canthwelem  10566  gchdju1  10572  pwfseqlem4  10578  gchdjuidm  10584  gchxpidm  10585  tskwe2  10689  rankcf  10693  tskuni  10699  gruxp  10723  dmrecnq  10884  lterpq  10886  archnq  10896  reclem3pr  10965  reclem4pr  10966  0idsr  11013  lep1  11987  ledivp1  12049  negfi  12096  supaddc  12114  supmul1  12116  suprzcl  12577  uz11  12781  zmin  12862  zbtwnre  12864  rpnnen1lem4  12898  rpnnen1lem5  12899  xnegid  13158  supxrre  13247  infxrre  13257  eluzfz2  13453  fzsuc  13492  fzsuc2  13503  fzp1disj  13504  fzneuz  13529  nn0p1elfzo  13623  fllep1  13726  fraclt1  13727  fracle1  13728  fracge0  13729  flhalf  13755  ceige  13769  ceim1l  13772  fldiv  13785  modval  13796  suppssfz  13922  seqeq1  13932  expubnd  14106  iexpcyc  14135  binom2sub1  14149  faclbnd4lem3  14223  pfxid  14613  pfxccatpfx2  14665  swrdccat3blem  14667  cshw0  14722  cshwn  14725  cshimadifsn  14757  cshimadifsn0  14758  pfx2  14875  trclexlem  14922  shftfval  14998  shftcan1  15011  reval  15034  cjmulrcl  15072  addcj  15076  absval  15166  absneg  15205  abscj  15207  sqabsadd  15210  sqabssub  15211  leabs  15227  sqreulem  15288  lo1res  15487  o1of2  15541  o1rlimmul  15547  flo1  15782  trirecip  15791  efcan  16024  efi4p  16067  resin4p  16068  recos4p  16069  sincossq  16106  ruclem10  16169  iddvds  16201  1dvds  16202  2ebits  16379  lcmftp  16568  coprmgcdb  16581  1idssfct  16612  exprmfct  16636  eulerthlem2  16714  odzphi  16729  pcprendvds  16773  pcmpt  16825  oddprmdvds  16836  vdwlem8  16921  0ram2  16954  prmgaplem7  16990  setsn0fun  17105  setsexstruct2  17107  pwsvscaval  17421  2initoinv  17939  initoeu1  17940  initoeu2lem1  17943  initoeu2  17945  2termoinv  17946  termoeu1  17947  homarel  17965  joinfval  18299  meetfval  18313  latjcom  18375  latmcom  18391  0subm  18747  sgrp2nmndlem5  18859  grprcan  18908  isgrpid2  18911  grpinvid  18934  mulgnn0z  19036  qus0  19123  eqg0subg  19130  ghmker  19176  symgbasmap  19311  symginv  19336  pmtrfrn  19392  odmulg2  19489  slwpgp  19547  pj1eq  19634  efgtf  19656  frgpinv  19698  frgpup2  19710  cnaddablx  19802  cnaddabl  19803  zaddablx  19806  imasabl  19810  dprdfadd  19956  dpjidcl  19994  dpjlid  19997  pgpfac1lem3  20013  omndmul2  20067  omndmul  20069  srgen1zr  20156  1unit  20315  unitgrpid  20326  1rinv  20336  irredn0  20364  irredneg  20371  c0snmgmhm  20403  rngisomring1  20409  zrrnghm  20474  rnrhmsubrg  20543  zrinitorngc  20580  zrtermorngc  20581  zrtermoringc  20613  isdrng2  20681  ringen1zr  20716  abv0  20761  abv1z  20762  abvneg  20764  orng0le1  20812  lmodfopne  20856  lsssn0  20904  lspsn0  20964  lsp0  20965  lmhmvsca  21002  lmhmrnlss  21007  lmhmkerlss  21008  lsppratlem5  21111  rsp1  21197  kerlidl  21238  ring2idlqus  21269  rngqiprngfulem4  21274  rngqiprngfu  21277  cnfldneg  21355  zringcyg  21429  chrid  21485  chrrhm  21491  ip0r  21597  ocvlss  21632  ocv1  21639  rlmassa  21831  psrbagfsupp  21880  snifpsrbag  21881  psrbaglefi  21887  psrvscaval  21911  psrdi  21925  psrdir  21926  mplvscaval  21976  mhpmpl  22092  mhpdeg  22093  mhppwdeg  22098  psdmul  22114  psdpw  22118  coe1sclmulfv  22230  coe1id  22242  ply1idvr1OLD  22244  evl1var  22285  mamuvs1  22354  mamuvs2  22355  matecl  22374  matvscacell  22385  mat0scmat  22487  submaval0  22529  mdetrsca  22552  maduval  22587  minmar1val0  22596  pmatcollpw3fi1lem2  22736  chcoeffeqlem  22834  cayleyhamilton0  22838  cayleyhamiltonALT  22840  toponsspwpw  22871  cctop  22955  cldval  22972  ntrfval  22973  clsfval  22974  cmclsopn  23011  opncldf3  23035  neifval  23048  lpfval  23087  cnrmnrm  23310  dis2ndc  23409  islocfin  23466  tx1cn  23558  idqtop  23655  kqtopon  23676  kqid  23677  kqcld  23684  hmphen2  23748  filssufil  23861  ufileu  23868  alexsublem  23993  efmndtmd  24050  symgtgp  24055  ustuqtop4  24193  cstucnd  24232  metustexhalf  24505  nm0  24578  rlmnlm  24637  nmolb  24666  metdseq0  24804  pi1xfrval  25015  clmvneg1  25060  clmvsubval  25070  ipcau2  25195  tcphcphlem1  25196  tcphcphlem2  25197  cmetcaulem  25249  ovolicc2lem3  25481  ovolicc2lem4  25482  mbfmulc2lem  25609  i1fpos  25668  mbfi1fseqlem3  25679  itg2ge0  25697  bddiblnc  25804  dvres2  25874  dvaddbr  25901  dvmulbr  25902  dvmulbrOLD  25903  dvcobr  25910  dvcobrOLD  25911  dvfsumlem4  25997  ftc1a  26005  ftc1lem6  26009  uc1pmon1p  26118  ig1pval2  26143  dgradd2  26235  dgrcolem2  26241  plydivlem4  26265  plydiveu  26267  elqaalem3  26290  qaa  26292  ulmdvlem1  26370  abelthlem6  26407  abelthlem7  26409  eflogeq  26572  jensenlem2  26959  harmonicbnd4  26982  sgmnncl  27118  dchrptlem2  27237  1lgs  27312  lgs1  27313  2sqcoprm  27407  addsqnreup  27415  dchrisumlem2  27462  dchrisum0lem2a  27489  selberg2lem  27522  pntrsumo1  27537  pntrsumbnd  27538  pntpbnd1  27558  pntlemr  27574  pntlemj  27575  padicabvf  27603  bdayval  27621  noextendgt  27643  nosupbnd2lem1  27688  noinfbnd2lem1  27703  noetainflem4  27713  oldval  27835  divmuls  28222  divscl  28224  seqsp1  28312  bdayfinbndlem1  28468  zz12s  28476  remulscllem1  28501  incistruhgr  29157  subgrprop3  29354  subgruhgredgd  29362  usgrexi  29519  cusgrexi  29521  cusgrsizeinds  29531  vtxdgfusgrf  29576  1hevtxdg1  29585  1egrvtxdg1  29588  ewlkprop  29682  wlklenvm1  29700  wlkl1loop  29716  wlkp1lem4  29753  2pthnloop  29809  upgrclwlkcompim  29859  crctcshwlkn0lem4  29891  crctcshwlkn0lem5  29892  crctcshwlkn0lem6  29893  crctcshwlkn0lem7  29894  crctcshlem4  29898  wspthnonp  29937  wlkswwlksf1o  29957  wwlksnwwlksnon  29993  umgr2wlkon  30028  wwlks2onv  30031  elwwlks2ons3im  30032  elwspths2spth  30048  umgrclwwlkge2  30071  clwlkclwwlkf1lem3  30086  erclwwlkref  30100  clwwlknp  30117  wwlksext2clwwlk  30137  wwlksubclwwlk  30138  0pthon1  30208  1wlkdlem4  30220  1pthd  30223  3spthd  30256  eupth2eucrct  30297  eucrctshift  30323  eucrct2eupth  30325  frgrncvvdeqlem8  30386  frgr2wwlkeqm  30411  isgrpoi  30578  grpoinvfval  30602  grpodivfval  30614  vcz  30655  cnaddabloOLD  30661  nvz0  30748  sspz  30815  lno0  30836  nmobndi  30855  ipasslem2  30912  shunssi  31448  ococin  31488  ssjo  31527  pjocini  31778  nlfnval  31961  lncnopbd  32117  riesz3i  32142  cnlnadjlem7  32153  pjclem4  32279  pj3si  32287  hstoc  32302  hstnmoc  32303  hstoh  32312  hst0  32313  mdsl2i  32402  chirredlem3  32472  chirredlem4  32473  dmdbr5ati  32502  rexunirn  32570  fcnvgreu  32754  infxrge0glb  32848  sgnneg  32917  cycpmco2lem5  33216  cycpmco2lem6  33217  cycpmco2lem7  33218  isarchi3  33273  nsgqusf1olem2  33499  ssdifidllem  33541  ssmxidllem  33558  rprmdvdspow  33618  ressply1sub  33655  fedgmullem1  33799  extdg1id  33836  nn0constr  33931  zartopn  34045  zarcmplem  34051  esumcvg  34256  esumcvgre  34261  sigaval  34281  unelldsys  34328  fiunelros  34344  measval  34368  pmeasmono  34494  probfinmeasb  34598  ballotlemfc0  34663  ballotlemfcc  34664  ballotlemsi  34685  ballotlemfrci  34698  signlem0  34757  breprexp  34803  bnj1006  35129  bnj1110  35151  bnj1253  35186  bnj1280  35189  bnj1463  35224  bnj1312  35227  fineqvinfep  35294  erdszelem7  35404  erdszelem8  35405  cvmliftlem10  35501  cvmliftlem13  35503  cvmlift2lem9  35518  cvmlift3lem6  35531  cvmlift3lem7  35532  cvmlift3lem9  35534  satfv1lem  35569  dfrdg2  36000  cldregopn  36538  tailfval  36579  filnetlem3  36587  filnetlem4  36588  ontopbas  36635  bj-elid4  37386  bj-imdiridlem  37403  f1omptsnlem  37554  icoreunrn  37577  relowlpssretop  37582  fvineqsnf1  37628  wl-sbal2  37782  unccur  37817  poimirlem1  37835  poimirlem2  37836  poimirlem4  37838  poimirlem6  37840  poimirlem7  37841  poimirlem11  37845  poimirlem12  37846  poimirlem17  37851  poimirlem20  37854  poimirlem22  37856  poimirlem23  37857  poimirlem28  37862  poimir  37867  ismblfin  37875  cnambfre  37882  ftc1cnnc  37906  dvasin  37918  ismtyres  38022  heiborlem8  38032  ghomidOLD  38103  rngosn6  38140  rngonegmn1l  38155  rngonegmn1r  38156  rngoneglmul  38157  rngonegrmul  38158  idlnegcl  38236  0idl  38239  0rngo  38241  smprngopr  38266  sucmapsuc  38703  cossex  38723  qsdisjALTV  38913  cnvepresdmqss  38951  mpets2  39169  lkrval  39427  ldualvaddval  39470  ldualvsval  39477  opoc1  39541  pmap0  40104  pmap1N  40106  pexmidALTN  40317  cdleme31fv  40729  cdlemg27b  41035  erngdvlem4  41330  erng0g  41333  erngdvlem4-rN  41338  dvalveclem  41364  dvh0g  41450  dih0cnv  41622  dih1rn  41626  dih1cnv  41627  doch0  41697  doch1  41698  lcfl7lem  41838  mapdheq  42067  hdmap1eq  42140  hdmapval2lem  42170  hgmapvvlem3  42264  zndvdchrrhm  42305  lcmineqlem13  42374  aks4d1p9  42421  primrootsunit1  42430  aks6d1c1p1  42440  aks6d1c1p6  42447  aks6d1c1p8  42448  sticksstones1  42479  sticksstones6  42484  sticksstones7  42485  sticksstones11  42489  sticksstones12a  42490  sticksstones12  42491  sticksstones22  42501  aks6d1c6isolem1  42507  aks6d1c6isolem2  42508  unitscyglem5  42532  renegid  42706  sn-0ne2  42739  remul01  42740  remulinvcom  42766  sn-0tie0  42784  renegmulnnass  42798  domnexpgn0cl  42856  abvexp  42865  frlmsnic  42873  fsuppssind  42914  mzpval  43052  mzpindd  43066  pellex  43155  2nn0ind  43265  jm2.26lem3  43321  pw2f1o2val  43359  wepwsolem  43362  fnwe2lem3  43372  lnmfg  43402  dgrsub2  43455  mpaaeu  43470  flcidc  43490  dflim5  43649  naddwordnexlem1  43717  rtrclexlem  43935  cnvrcl0  43944  brcoffn  44349  clsk1indlem3  44362  clsneif1o  44423  clsneicnv  44424  clsneikex  44425  clsneinex  44426  neicvgmex  44436  neicvgel1  44438  suprleubrd  44485  suprlubrd  44487  imo72b2  44491  dvconstbi  44653  bcc0  44659  binomcxplemnotnn0  44675  nnfoctb  45371  infleinflem1  45691  fprodcnlem  45922  sumnnodd  45953  icccncfext  46208  itgsin0pilem1  46271  stoweidlem32  46353  stoweidlem35  46356  stoweidlem36  46357  stoweidlem37  46358  stoweidlem43  46364  stoweidlem50  46371  wallispilem5  46390  stirlinglem2  46396  stirlinglem3  46397  stirlinglem4  46398  stirlinglem8  46402  stirlinglem11  46405  stirlinglem12  46406  stirlinglem14  46408  stirlinglem15  46409  fourierdlem11  46439  fourierdlem20  46448  fourierdlem21  46449  fourierdlem41  46469  fourierdlem42  46470  fourierdlem48  46475  fourierdlem49  46476  fourierdlem64  46491  fourierdlem71  46498  fourierdlem79  46506  fourierdlem90  46517  fourierdlem91  46518  fourierswlem  46551  etransclem17  46572  etransclem38  46593  saluni  46646  meaiininclem  46807  issmflelem  47065  issmfgtlem  47076  issmfgelem  47090  smflimsuplem4  47144  f1cof1blem  47397  zplusmodne  47666  m1modne  47671  submodneaddmod  47674  sprval  47802  prprval  47837  bgoldbtbndlem2  48129  bgoldbtbndlem3  48130  bgoldbtbnd  48132  isubgrvtxuhgr  48187  isubgredg  48189  grimcnv  48211  isuspgrim  48219  gricushgr  48240  uhgrimisgrgric  48254  grtriclwlk3  48268  isubgr3stgrlem7  48295  grlimgrtri  48326  grlictr  48338  gpgvtx0  48376  gpgvtx1  48377  gpgprismgrusgra  48381  gpgedgvtx1  48385  gpg3kgrtriex  48412  pgnbgreunbgrlem3  48441  pgnbgreunbgrlem6  48447  isclintop  48530  clintopcllaw  48534  nzrneg1ne0  48553  lidldomn1  48554  zlidlring  48557  uzlidlring  48558  2zrngnmlid  48578  cznrng  48584  blenre  48897  blennn  48898  2arymaptf  48975  itcoval1  48986  itcovalendof  48992  ehl2eudisval0  49048  eenglngeehlnmlem2  49061  itsclc0yqsol  49087  inlinecirc02plem  49109  ipolub  49310  ipoglb  49313  nelsubclem  49389  imaid  49476  imaf1co  49477  uptri  49536  uptrar  49538  uptrai  49539  oppc1stflem  49609  setrec2mpt  50019