Theorem mpdan 684

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 396

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 397

This theorem is referenced by:  mpidan  686  mpan2  688  biadanid  820  mpjaodan  956  mpjao3dan  1430  mpd3an3  1461  elabd2  3602  eueq2  3646  csbiegf  3867  difsnb  4740  reusv3i  5328  frpoinsg  6250  fimadmfo  6706  fimadmfoALT  6708  fvtresfn  6886  fvmpt3  6888  ffvelrnd  6971  fnressn  7039  fsnex  7164  f1oiso2  7232  riota5f  7270  suceloni  7668  onsucuni  7684  frrlem10  8120  seqomlem2  8291  oaordi  8386  nnaordi  8458  qsdisj  8592  dom2lem  8789  canth2g  8927  limenpsi  8948  nnfi  8959  php4  9005  onfin  9022  sucdom  9027  sucxpdom  9041  xpfi  9094  dmfi  9106  pwfilemOLD  9122  pwfiOLD  9123  fiin  9190  supiso  9243  ordiso2  9283  wdom2d  9348  infeq5  9404  cantnfp1lem3  9447  cantnflem1d  9455  rankwflemb  9560  onenon  9716  cardonle  9724  sdomsdomcardi  9738  acni  9810  cardaleph  9854  djuen  9934  djuinf  9953  infdju1  9954  nnadju  9962  pwsdompw  9969  infdif  9974  cfval  10012  fin34  10155  fin1a2lem1  10165  fin1a2  10180  ttukeylem6  10279  sdomsdomcard  10325  canth3  10326  fpwwe2  10408  canthwelem  10415  gchdju1  10421  pwfseqlem4  10427  gchdjuidm  10433  gchxpidm  10434  tskwe2  10538  rankcf  10542  tskuni  10548  gruxp  10572  dmrecnq  10733  lterpq  10735  archnq  10745  reclem3pr  10814  reclem4pr  10815  0idsr  10862  lep1  11825  ledivp1  11886  negfi  11933  supaddc  11951  supmul1  11953  suprzcl  12409  uz11  12616  zmin  12693  zbtwnre  12695  rpnnen1lem4  12729  rpnnen1lem5  12730  xnegid  12981  supxrre  13070  infxrre  13079  eluzfz2  13273  fzsuc  13312  fzsuc2  13323  fzp1disj  13324  fzneuz  13346  nn0p1elfzo  13439  fllep1  13530  fraclt1  13531  fracle1  13532  fracge0  13533  flhalf  13559  ceige  13573  ceim1l  13576  fldiv  13589  modval  13600  suppssfz  13723  seqeq1  13733  expubnd  13904  iexpcyc  13932  binom2sub1  13945  faclbnd4lem3  14018  pfxid  14406  pfxccatpfx2  14459  swrdccat3blem  14461  cshw0  14516  cshwn  14519  cshimadifsn  14551  cshimadifsn0  14552  pfx2  14669  trclexlem  14714  shftfval  14790  shftcan1  14803  reval  14826  cjmulrcl  14864  addcj  14868  absval  14958  absneg  14998  abscj  15000  sqabsadd  15003  sqabssub  15004  leabs  15020  sqreulem  15080  lo1res  15277  o1of2  15331  o1rlimmul  15337  flo1  15575  trirecip  15584  efcan  15814  efi4p  15855  resin4p  15856  recos4p  15857  sincossq  15894  ruclem10  15957  iddvds  15988  1dvds  15989  2ebits  16163  lcmftp  16350  coprmgcdb  16363  1idssfct  16394  exprmfct  16418  eulerthlem2  16492  odzphi  16506  pcprendvds  16550  pcmpt  16602  oddprmdvds  16613  vdwlem8  16698  0ram2  16731  prmgaplem7  16767  setsn0fun  16883  setsexstruct2  16885  pwsvscaval  17215  2initoinv  17734  initoeu1  17735  initoeu2lem1  17738  initoeu2  17740  2termoinv  17741  termoeu1  17742  homarel  17760  joinfval  18100  meetfval  18114  latjcom  18174  latmcom  18190  0subm  18465  sgrp2nmndlem5  18577  grprcan  18622  isgrpid2  18625  grpinvid  18645  mulgnn0z  18739  0subg  18789  qus0  18823  ghmker  18869  symgbasmap  18993  symginv  19019  pmtrfrn  19075  odmulg2  19171  slwpgp  19227  pj1eq  19315  efgtf  19337  frgpinv  19379  frgpup2  19391  cnaddablx  19478  cnaddabl  19479  zaddablx  19482  dprdfadd  19632  dpjidcl  19670  dpjlid  19673  pgpfac1lem3  19689  srgen1zr  19775  1unit  19909  unitgrpid  19920  1rinv  19930  irredn0  19954  irredneg  19961  isdrng2  20010  rnrhmsubrg  20065  abv0  20100  abv1z  20101  abvneg  20103  lmodfopne  20170  lsssn0  20218  lspsn0  20279  lsp0  20280  lmhmvsca  20316  lmhmrnlss  20321  lmhmkerlss  20322  lsppratlem5  20422  rsp1  20504  ringen1zr  20557  cnfldneg  20633  zringcyg  20700  chrid  20740  chrrhm  20744  ip0r  20851  ocvlss  20886  ocv1  20893  rlmassa  21084  psrbagfsupp  21132  snifpsrbag  21134  psrbaglefi  21144  psrvscaval  21170  psrdi  21184  psrdir  21185  mplvscaval  21229  mhpmpl  21343  mhpdeg  21344  mhppwdeg  21349  coe1sclmulfv  21463  ply1idvr1  21473  evl1var  21511  mamuvs1  21561  mamuvs2  21562  matecl  21583  matvscacell  21594  mat0scmat  21696  submaval0  21738  mdetrsca  21761  maduval  21796  minmar1val0  21805  pmatcollpw3fi1lem2  21945  chcoeffeqlem  22043  cayleyhamilton0  22047  cayleyhamiltonALT  22049  toponsspwpw  22080  cctop  22165  cldval  22183  ntrfval  22184  clsfval  22185  cmclsopn  22222  opncldf3  22246  neifval  22259  lpfval  22298  cnrmnrm  22521  dis2ndc  22620  islocfin  22677  tx1cn  22769  idqtop  22866  kqtopon  22887  kqid  22888  kqcld  22895  hmphen2  22959  filssufil  23072  ufileu  23079  alexsublem  23204  efmndtmd  23261  symgtgp  23266  ustuqtop4  23405  cstucnd  23445  metustexhalf  23721  nm0  23794  rlmnlm  23861  nmolb  23890  metdseq0  24026  pi1xfrval  24226  clmvneg1  24271  clmvsubval  24281  ipcau2  24407  tcphcphlem1  24408  tcphcphlem2  24409  cmetcaulem  24461  ovolicc2lem3  24692  ovolicc2lem4  24693  mbfmulc2lem  24820  i1fpos  24880  mbfi1fseqlem3  24891  itg2ge0  24909  bddiblnc  25015  dvres2  25085  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvfsumlem4  25202  ftc1a  25210  ftc1lem6  25214  uc1pmon1p  25325  ig1pval2  25347  dgradd2  25438  dgrcolem2  25444  plydivlem4  25465  plydiveu  25467  elqaalem3  25490  qaa  25492  ulmdvlem1  25568  abelthlem6  25604  abelthlem7  25606  eflogeq  25766  jensenlem2  26146  harmonicbnd4  26169  sgmnncl  26305  dchrptlem2  26422  1lgs  26497  lgs1  26498  2sqcoprm  26592  addsqnreup  26600  dchrisumlem2  26647  dchrisum0lem2a  26674  selberg2lem  26707  pntrsumo1  26722  pntrsumbnd  26723  pntpbnd1  26743  pntlemr  26759  pntlemj  26760  padicabvf  26788  incistruhgr  27458  subgrprop3  27652  subgruhgredgd  27660  usgrexi  27817  cusgrexi  27819  cusgrsizeinds  27828  vtxdgfusgrf  27873  1hevtxdg1  27882  1egrvtxdg1  27885  ewlkprop  27979  wlklenvm1  27998  wlkl1loop  28014  wlkp1lem4  28053  2pthnloop  28108  upgrclwlkcompim  28158  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  crctcshwlkn0lem7  28190  crctcshlem4  28194  wspthnonp  28233  wlkswwlksf1o  28253  wwlksnwwlksnon  28289  umgr2wlkon  28324  wwlks2onv  28327  elwwlks2ons3im  28328  elwspths2spth  28341  umgrclwwlkge2  28364  clwlkclwwlkf1lem3  28379  erclwwlkref  28393  clwwlknp  28410  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  0pthon1  28501  1wlkdlem4  28513  1pthd  28516  3spthd  28549  eupth2eucrct  28590  eucrctshift  28616  eucrct2eupth  28618  frgrncvvdeqlem8  28679  frgr2wwlkeqm  28704  isgrpoi  28869  grpoinvfval  28893  grpodivfval  28905  vcz  28946  cnaddabloOLD  28952  nvz0  29039  sspz  29106  lno0  29127  nmobndi  29146  ipasslem2  29203  shunssi  29739  ococin  29779  ssjo  29818  pjocini  30069  nlfnval  30252  lncnopbd  30408  riesz3i  30433  cnlnadjlem7  30444  pjclem4  30570  pj3si  30578  hstoc  30593  hstnmoc  30594  hstoh  30603  hst0  30604  mdsl2i  30693  chirredlem3  30763  chirredlem4  30764  dmdbr5ati  30793  rexunirn  30849  fcnvgreu  31019  infxrge0glb  31097  omndmul2  31347  omndmul  31349  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  isarchi3  31450  orng0le1  31520  nsgqusf1olem2  31608  kerlidl  31613  ssmxidllem  31650  fedgmullem1  31719  extdg1id  31747  zartopn  31834  zarcmplem  31840  esumcvg  32063  esumcvgre  32068  sigaval  32088  unelldsys  32135  fiunelros  32151  measval  32175  pmeasmono  32300  probfinmeasb  32404  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsi  32490  ballotlemfrci  32503  sgnneg  32516  signlem0  32575  breprexp  32622  bnj1006  32949  bnj1110  32971  bnj1253  33006  bnj1280  33009  bnj1463  33044  bnj1312  33047  erdszelem7  33168  erdszelem8  33169  cvmliftlem10  33265  cvmliftlem13  33267  cvmlift2lem9  33282  cvmlift3lem6  33295  cvmlift3lem7  33296  cvmlift3lem9  33298  satfv1lem  33333  dfrdg2  33780  bdayval  33860  noextendgt  33882  nosupbnd2lem1  33927  noinfbnd2lem1  33942  noetainflem4  33952  oldval  34047  cldregopn  34529  tailfval  34570  filnetlem3  34578  filnetlem4  34579  ontopbas  34626  bj-elid4  35348  bj-imdiridlem  35365  f1omptsnlem  35516  icoreunrn  35539  relowlpssretop  35544  fvineqsnf1  35590  wl-sbal2  35728  unccur  35769  poimirlem1  35787  poimirlem2  35788  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem17  35803  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem28  35814  poimir  35819  ismblfin  35827  cnambfre  35834  ftc1cnnc  35858  dvasin  35870  ismtyres  35975  heiborlem8  35985  ghomidOLD  36056  rngosn6  36093  rngonegmn1l  36108  rngonegmn1r  36109  rngoneglmul  36110  rngonegrmul  36111  idlnegcl  36189  0idl  36192  0rngo  36194  smprngopr  36219  cossex  36549  qsdisjALTV  36735  cnvepresdmqss  36771  lkrval  37109  ldualvaddval  37152  ldualvsval  37159  opoc1  37223  pmap0  37786  pmap1N  37788  pexmidALTN  37999  cdleme31fv  38411  cdlemg27b  38717  erngdvlem4  39012  erng0g  39015  erngdvlem4-rN  39020  dvalveclem  39046  dvh0g  39132  dih0cnv  39304  dih1rn  39308  dih1cnv  39309  doch0  39379  doch1  39380  lcfl7lem  39520  mapdheq  39749  hdmap1eq  39822  hdmapval2lem  39852  hgmapvvlem3  39946  lcmineqlem13  40056  aks4d1p9  40103  sticksstones1  40109  sticksstones6  40114  sticksstones7  40115  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  frlmsnic  40270  fsuppssind  40289  renegid  40363  sn-0ne2  40396  remul01  40397  remulinvcom  40421  sn-0tie0  40428  sn-inelr  40442  mzpval  40561  mzpindd  40575  pellex  40664  2nn0ind  40774  jm2.26lem3  40830  pw2f1o2val  40868  wepwsolem  40874  fnwe2lem3  40884  lnmfg  40914  dgrsub2  40967  mpaaeu  40982  flcidc  41006  rtrclexlem  41231  cnvrcl0  41240  brcoffn  41647  clsk1indlem3  41660  clsneif1o  41721  clsneicnv  41722  clsneikex  41723  clsneinex  41724  neicvgmex  41734  neicvgel1  41736  suprleubrd  41784  suprlubrd  41786  imo72b2  41790  dvconstbi  41959  bcc0  41965  binomcxplemnotnn0  41981  nnfoctb  42602  infleinflem1  42916  fprodcnlem  43147  sumnnodd  43178  icccncfext  43435  itgsin0pilem1  43498  stoweidlem32  43580  stoweidlem35  43583  stoweidlem36  43584  stoweidlem37  43585  stoweidlem43  43591  stoweidlem50  43598  wallispilem5  43617  stirlinglem2  43623  stirlinglem3  43624  stirlinglem4  43625  stirlinglem8  43629  stirlinglem11  43632  stirlinglem12  43633  stirlinglem14  43635  stirlinglem15  43636  fourierdlem11  43666  fourierdlem20  43675  fourierdlem21  43676  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem64  43718  fourierdlem71  43725  fourierdlem79  43733  fourierdlem90  43744  fourierdlem91  43745  fourierswlem  43778  etransclem17  43799  etransclem38  43820  saluni  43872  meaiininclem  44031  issmflelem  44289  issmfgtlem  44300  issmfgelem  44314  smflimsuplem4  44367  f1cof1blem  44579  sprval  44942  prprval  44977  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  isomushgr  45289  isomuspgrlem1  45290  isclintop  45412  clintopcllaw  45416  nzrneg1ne0  45438  c0snmgmhm  45483  zrrnghm  45486  lidldomn1  45490  zlidlring  45497  uzlidlring  45498  2zrngnmlid  45518  cznrng  45524  zrinitorngc  45569  zrtermorngc  45570  zrtermoringc  45639  coe1id  45736  blenre  45931  blennn  45932  2arymaptf  46009  itcoval1  46020  itcovalendof  46026  ehl2eudisval0  46082  eenglngeehlnmlem2  46095  itsclc0yqsol  46121  inlinecirc02plem  46143  ipolub  46285  ipoglb  46288