Theorem mpdan 686

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 397

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 206  df-an 398

This theorem is referenced by:  mpidan  688  mpan2  690  biadanid  822  mpjaodan  958  mpjao3dan  1432  mpd3an3  1463  elabd2  3660  eueq2  3706  csbiegf  3927  difsnb  4809  reusv3i  5402  frpoinsg  6342  fimadmfo  6812  fimadmfoALT  6814  fvtresfn  6998  fvmpt3  7000  ffvelcdmd  7085  fnressn  7153  fsnex  7278  f1oiso2  7346  riota5f  7391  onsuc  7796  onsucuni  7813  frrlem10  8277  seqomlem2  8448  oaordi  8543  nnaordi  8615  qsdisj  8785  dom2lem  8985  canth2g  9128  limenpsi  9149  nnfi  9164  php4  9210  onfin  9227  sucxpdom  9252  xpfiOLD  9315  dmfi  9327  pwfilemOLD  9343  pwfiOLD  9344  fiin  9414  supiso  9467  ordiso2  9507  wdom2d  9572  infeq5  9629  cantnfp1lem3  9672  cantnflem1d  9680  rankwflemb  9785  onenon  9941  cardonle  9949  sdomsdomcardi  9963  acni  10037  cardaleph  10081  djuen  10161  djuinf  10180  infdju1  10181  nnadju  10189  pwsdompw  10196  infdif  10201  cfval  10239  fin34  10382  fin1a2lem1  10392  fin1a2  10407  ttukeylem6  10506  sdomsdomcard  10552  canth3  10553  fpwwe2  10635  canthwelem  10642  gchdju1  10648  pwfseqlem4  10654  gchdjuidm  10660  gchxpidm  10661  tskwe2  10765  rankcf  10769  tskuni  10775  gruxp  10799  dmrecnq  10960  lterpq  10962  archnq  10972  reclem3pr  11041  reclem4pr  11042  0idsr  11089  lep1  12052  ledivp1  12113  negfi  12160  supaddc  12178  supmul1  12180  suprzcl  12639  uz11  12844  zmin  12925  zbtwnre  12927  rpnnen1lem4  12961  rpnnen1lem5  12962  xnegid  13214  supxrre  13303  infxrre  13312  eluzfz2  13506  fzsuc  13545  fzsuc2  13556  fzp1disj  13557  fzneuz  13579  nn0p1elfzo  13672  fllep1  13763  fraclt1  13764  fracle1  13765  fracge0  13766  flhalf  13792  ceige  13806  ceim1l  13809  fldiv  13822  modval  13833  suppssfz  13956  seqeq1  13966  expubnd  14139  iexpcyc  14168  binom2sub1  14181  faclbnd4lem3  14252  pfxid  14631  pfxccatpfx2  14684  swrdccat3blem  14686  cshw0  14741  cshwn  14744  cshimadifsn  14777  cshimadifsn0  14778  pfx2  14895  trclexlem  14938  shftfval  15014  shftcan1  15027  reval  15050  cjmulrcl  15088  addcj  15092  absval  15182  absneg  15221  abscj  15223  sqabsadd  15226  sqabssub  15227  leabs  15243  sqreulem  15303  lo1res  15500  o1of2  15554  o1rlimmul  15560  flo1  15797  trirecip  15806  efcan  16036  efi4p  16077  resin4p  16078  recos4p  16079  sincossq  16116  ruclem10  16179  iddvds  16210  1dvds  16211  2ebits  16385  lcmftp  16570  coprmgcdb  16583  1idssfct  16614  exprmfct  16638  eulerthlem2  16712  odzphi  16726  pcprendvds  16770  pcmpt  16822  oddprmdvds  16833  vdwlem8  16918  0ram2  16951  prmgaplem7  16987  setsn0fun  17103  setsexstruct2  17105  pwsvscaval  17438  2initoinv  17957  initoeu1  17958  initoeu2lem1  17961  initoeu2  17963  2termoinv  17964  termoeu1  17965  homarel  17983  joinfval  18323  meetfval  18337  latjcom  18397  latmcom  18413  0subm  18695  sgrp2nmndlem5  18807  grprcan  18855  isgrpid2  18858  grpinvid  18881  mulgnn0z  18976  0subgOLD  19027  qus0  19063  eqg0subg  19068  ghmker  19113  symgbasmap  19239  symginv  19265  pmtrfrn  19321  odmulg2  19418  slwpgp  19476  pj1eq  19563  efgtf  19585  frgpinv  19627  frgpup2  19639  cnaddablx  19731  cnaddabl  19732  zaddablx  19735  imasabl  19739  dprdfadd  19885  dpjidcl  19923  dpjlid  19926  pgpfac1lem3  19942  srgen1zr  20033  1unit  20181  unitgrpid  20192  1rinv  20202  irredn0  20230  irredneg  20237  isdrng2  20322  ringen1zr  20350  rnrhmsubrg  20390  abv0  20432  abv1z  20433  abvneg  20435  lmodfopne  20503  lsssn0  20551  lspsn0  20612  lsp0  20613  lmhmvsca  20649  lmhmrnlss  20654  lmhmkerlss  20655  lsppratlem5  20757  rsp1  20842  cnfldneg  20964  zringcyg  21031  chrid  21071  chrrhm  21075  ip0r  21182  ocvlss  21217  ocv1  21224  rlmassa  21417  psrbagfsupp  21465  snifpsrbag  21467  psrbaglefi  21477  psrvscaval  21503  psrdi  21518  psrdir  21519  mplvscaval  21567  mhpmpl  21679  mhpdeg  21680  mhppwdeg  21685  coe1sclmulfv  21797  ply1idvr1  21809  evl1var  21847  mamuvs1  21897  mamuvs2  21898  matecl  21919  matvscacell  21930  mat0scmat  22032  submaval0  22074  mdetrsca  22097  maduval  22132  minmar1val0  22141  pmatcollpw3fi1lem2  22281  chcoeffeqlem  22379  cayleyhamilton0  22383  cayleyhamiltonALT  22385  toponsspwpw  22416  cctop  22501  cldval  22519  ntrfval  22520  clsfval  22521  cmclsopn  22558  opncldf3  22582  neifval  22595  lpfval  22634  cnrmnrm  22857  dis2ndc  22956  islocfin  23013  tx1cn  23105  idqtop  23202  kqtopon  23223  kqid  23224  kqcld  23231  hmphen2  23295  filssufil  23408  ufileu  23415  alexsublem  23540  efmndtmd  23597  symgtgp  23602  ustuqtop4  23741  cstucnd  23781  metustexhalf  24057  nm0  24130  rlmnlm  24197  nmolb  24226  metdseq0  24362  pi1xfrval  24562  clmvneg1  24607  clmvsubval  24617  ipcau2  24743  tcphcphlem1  24744  tcphcphlem2  24745  cmetcaulem  24797  ovolicc2lem3  25028  ovolicc2lem4  25029  mbfmulc2lem  25156  i1fpos  25216  mbfi1fseqlem3  25227  itg2ge0  25245  bddiblnc  25351  dvres2  25421  dvaddbr  25447  dvmulbr  25448  dvcobr  25455  dvfsumlem4  25538  ftc1a  25546  ftc1lem6  25550  uc1pmon1p  25661  ig1pval2  25683  dgradd2  25774  dgrcolem2  25780  plydivlem4  25801  plydiveu  25803  elqaalem3  25826  qaa  25828  ulmdvlem1  25904  abelthlem6  25940  abelthlem7  25942  eflogeq  26102  jensenlem2  26482  harmonicbnd4  26505  sgmnncl  26641  dchrptlem2  26758  1lgs  26833  lgs1  26834  2sqcoprm  26928  addsqnreup  26936  dchrisumlem2  26983  dchrisum0lem2a  27010  selberg2lem  27043  pntrsumo1  27058  pntrsumbnd  27059  pntpbnd1  27079  pntlemr  27095  pntlemj  27096  padicabvf  27124  bdayval  27141  noextendgt  27163  nosupbnd2lem1  27208  noinfbnd2lem1  27223  noetainflem4  27233  oldval  27339  divsmul  27657  divscl  27659  incistruhgr  28329  subgrprop3  28523  subgruhgredgd  28531  usgrexi  28688  cusgrexi  28690  cusgrsizeinds  28699  vtxdgfusgrf  28744  1hevtxdg1  28753  1egrvtxdg1  28756  ewlkprop  28850  wlklenvm1  28869  wlkl1loop  28885  wlkp1lem4  28923  2pthnloop  28978  upgrclwlkcompim  29028  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  crctcshwlkn0lem6  29059  crctcshwlkn0lem7  29060  crctcshlem4  29064  wspthnonp  29103  wlkswwlksf1o  29123  wwlksnwwlksnon  29159  umgr2wlkon  29194  wwlks2onv  29197  elwwlks2ons3im  29198  elwspths2spth  29211  umgrclwwlkge2  29234  clwlkclwwlkf1lem3  29249  erclwwlkref  29263  clwwlknp  29280  wwlksext2clwwlk  29300  wwlksubclwwlk  29301  0pthon1  29371  1wlkdlem4  29383  1pthd  29386  3spthd  29419  eupth2eucrct  29460  eucrctshift  29486  eucrct2eupth  29488  frgrncvvdeqlem8  29549  frgr2wwlkeqm  29574  isgrpoi  29739  grpoinvfval  29763  grpodivfval  29775  vcz  29816  cnaddabloOLD  29822  nvz0  29909  sspz  29976  lno0  29997  nmobndi  30016  ipasslem2  30073  shunssi  30609  ococin  30649  ssjo  30688  pjocini  30939  nlfnval  31122  lncnopbd  31278  riesz3i  31303  cnlnadjlem7  31314  pjclem4  31440  pj3si  31448  hstoc  31463  hstnmoc  31464  hstoh  31473  hst0  31474  mdsl2i  31563  chirredlem3  31633  chirredlem4  31634  dmdbr5ati  31663  rexunirn  31720  fcnvgreu  31886  infxrge0glb  31966  omndmul2  32218  omndmul  32220  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  isarchi3  32321  orng0le1  32419  nsgqusf1olem2  32514  kerlidl  32527  ssmxidllem  32578  ressply1sub  32648  fedgmullem1  32703  extdg1id  32731  zartopn  32844  zarcmplem  32850  esumcvg  33073  esumcvgre  33078  sigaval  33098  unelldsys  33145  fiunelros  33161  measval  33185  pmeasmono  33312  probfinmeasb  33416  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemsi  33502  ballotlemfrci  33515  sgnneg  33528  signlem0  33587  breprexp  33634  bnj1006  33960  bnj1110  33982  bnj1253  34017  bnj1280  34020  bnj1463  34055  bnj1312  34058  erdszelem7  34177  erdszelem8  34178  cvmliftlem10  34274  cvmliftlem13  34276  cvmlift2lem9  34291  cvmlift3lem6  34304  cvmlift3lem7  34305  cvmlift3lem9  34307  satfv1lem  34342  dfrdg2  34756  gg-dvmulbr  35164  gg-dvcobr  35165  cldregopn  35205  tailfval  35246  filnetlem3  35254  filnetlem4  35255  ontopbas  35302  bj-elid4  36038  bj-imdiridlem  36055  f1omptsnlem  36206  icoreunrn  36229  relowlpssretop  36234  fvineqsnf1  36280  wl-sbal2  36418  unccur  36460  poimirlem1  36478  poimirlem2  36479  poimirlem4  36481  poimirlem6  36483  poimirlem7  36484  poimirlem11  36488  poimirlem12  36489  poimirlem17  36494  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  poimirlem28  36505  poimir  36510  ismblfin  36518  cnambfre  36525  ftc1cnnc  36549  dvasin  36561  ismtyres  36665  heiborlem8  36675  ghomidOLD  36746  rngosn6  36783  rngonegmn1l  36798  rngonegmn1r  36799  rngoneglmul  36800  rngonegrmul  36801  idlnegcl  36879  0idl  36882  0rngo  36884  smprngopr  36909  cossex  37278  qsdisjALTV  37474  cnvepresdmqss  37511  mpets2  37700  lkrval  37947  ldualvaddval  37990  ldualvsval  37997  opoc1  38061  pmap0  38625  pmap1N  38627  pexmidALTN  38838  cdleme31fv  39250  cdlemg27b  39556  erngdvlem4  39851  erng0g  39854  erngdvlem4-rN  39859  dvalveclem  39885  dvh0g  39971  dih0cnv  40143  dih1rn  40147  dih1cnv  40148  doch0  40218  doch1  40219  lcfl7lem  40359  mapdheq  40588  hdmap1eq  40661  hdmapval2lem  40691  hgmapvvlem3  40785  lcmineqlem13  40895  aks4d1p9  40942  sticksstones1  40951  sticksstones6  40956  sticksstones7  40957  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  frlmsnic  41108  fsuppssind  41163  renegid  41243  sn-0ne2  41276  remul01  41277  remulinvcom  41302  sn-0tie0  41309  renegmulnnass  41323  sn-inelr  41335  mzpval  41456  mzpindd  41470  pellex  41559  2nn0ind  41670  jm2.26lem3  41726  pw2f1o2val  41764  wepwsolem  41770  fnwe2lem3  41780  lnmfg  41810  dgrsub2  41863  mpaaeu  41878  flcidc  41902  dflim5  42065  naddwordnexlem1  42134  rtrclexlem  42353  cnvrcl0  42362  brcoffn  42767  clsk1indlem3  42780  clsneif1o  42841  clsneicnv  42842  clsneikex  42843  clsneinex  42844  neicvgmex  42854  neicvgel1  42856  suprleubrd  42904  suprlubrd  42906  imo72b2  42910  dvconstbi  43079  bcc0  43085  binomcxplemnotnn0  43101  nnfoctb  43720  infleinflem1  44067  fprodcnlem  44302  sumnnodd  44333  icccncfext  44590  itgsin0pilem1  44653  stoweidlem32  44735  stoweidlem35  44738  stoweidlem36  44739  stoweidlem37  44740  stoweidlem43  44746  stoweidlem50  44753  wallispilem5  44772  stirlinglem2  44778  stirlinglem3  44779  stirlinglem4  44780  stirlinglem8  44784  stirlinglem11  44787  stirlinglem12  44788  stirlinglem14  44790  stirlinglem15  44791  fourierdlem11  44821  fourierdlem20  44830  fourierdlem21  44831  fourierdlem41  44851  fourierdlem42  44852  fourierdlem48  44857  fourierdlem49  44858  fourierdlem64  44873  fourierdlem71  44880  fourierdlem79  44888  fourierdlem90  44899  fourierdlem91  44900  fourierswlem  44933  etransclem17  44954  etransclem38  44975  saluni  45028  meaiininclem  45189  issmflelem  45447  issmfgtlem  45458  issmfgelem  45472  smflimsuplem4  45526  f1cof1blem  45771  sprval  46134  prprval  46169  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbnd  46464  isomushgr  46481  isomuspgrlem1  46482  isclintop  46604  clintopcllaw  46608  nzrneg1ne0  46630  c0snmgmhm  46699  zrrnghm  46702  ring2idlqus  46775  lidldomn1  46777  zlidlring  46780  uzlidlring  46781  2zrngnmlid  46801  cznrng  46807  zrinitorngc  46852  zrtermorngc  46853  zrtermoringc  46922  coe1id  47019  blenre  47214  blennn  47215  2arymaptf  47292  itcoval1  47303  itcovalendof  47309  ehl2eudisval0  47365  eenglngeehlnmlem2  47378  itsclc0yqsol  47404  inlinecirc02plem  47426  ipolub  47567  ipoglb  47570  setrec2mpt  47696