Theorem mpdan 695

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 592	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpidan  697  mpan2  699  biadanid  830  mpjaodan  969  mpjao3dan  1443  mpd3an3  1473  elabd2  3620  eueq2  3663  csbiegf  3876  difsnb  4756  reusv3i  5351  frpoinsg  6315  fimadmfo  6772  fimadmfoALT  6774  fvtresfn  6963  fvmpt3  6965  ffvelcdmd  7051  fnressn  7126  fsnex  7252  f1oiso2  7321  riota5f  7366  onsuc  7778  onsucuni  7793  frrlem10  8260  seqomlem2  8406  oaordi  8499  nnaordi  8572  qsdisj  8760  dom2lem  8958  canth2g  9088  limenpsi  9109  nnfi  9121  php4  9163  onfin  9168  sucxpdom  9190  dmfi  9264  fiin  9354  supiso  9408  ordiso2  9449  wdom2d  9514  elirrvOLD  9532  infeq5  9578  cantnfp1lem3  9621  cantnflem1d  9629  rankwflemb  9737  onenon  9893  cardonle  9901  sdomsdomcardi  9915  acni  9987  cardaleph  10031  djuen  10112  djuinf  10131  infdju1  10132  nnadju  10140  pwsdompw  10145  infdif  10150  cfval  10189  fin34  10333  fin1a2lem1  10343  fin1a2  10358  ttukeylem6  10457  sdomsdomcard  10503  canth3  10504  fpwwe2  10587  canthwelem  10594  gchdju1  10600  pwfseqlem4  10606  gchdjuidm  10612  gchxpidm  10613  tskwe2  10717  rankcf  10721  tskuni  10727  gruxp  10751  dmrecnq  10912  lterpq  10914  archnq  10924  reclem3pr  10993  reclem4pr  10994  0idsr  11041  lep1  12018  ledivp1  12080  negfi  12127  supaddc  12145  supmul1  12147  suprzcl  12639  uz11  12850  zmin  12931  zbtwnre  12933  rpnnen1lem4  12967  rpnnen1lem5  12968  xnegid  13227  supxrre  13316  infxrre  13326  eluzfz2  13523  fzsuc  13562  fzsuc2  13573  fzp1disj  13574  fzneuz  13599  nn0p1elfzo  13694  fllep1  13797  fraclt1  13798  fracle1  13799  fracge0  13800  flhalf  13826  ceige  13840  ceim1l  13843  fldiv  13856  modval  13867  suppssfz  13993  seqeq1  14003  expubnd  14177  iexpcyc  14206  binom2sub1  14220  faclbnd4lem3  14294  pfxid  14684  pfxccatpfx2  14736  swrdccat3blem  14738  cshw0  14793  cshwn  14796  cshimadifsn  14828  cshimadifsn0  14829  pfx2  14946  trclexlem  14993  shftfval  15069  shftcan1  15082  reval  15105  cjmulrcl  15143  addcj  15147  absval  15237  absneg  15276  abscj  15278  sqabsadd  15281  sqabssub  15282  leabs  15298  sqreulem  15359  lo1res  15558  o1of2  15612  o1rlimmul  15618  fsumconst1  15790  flo1  15856  trirecip  15865  efcan  16098  efi4p  16141  resin4p  16142  recos4p  16143  sincossq  16180  ruclem10  16243  iddvds  16275  1dvds  16276  2ebits  16453  lcmftp  16642  coprmgcdb  16655  1idssfct  16686  exprmfct  16711  eulerthlem2  16789  odzphi  16804  pcprendvds  16848  pcmpt  16900  oddprmdvds  16911  vdwlem8  16996  0ram2  17029  prmgaplem7  17065  setsn0fun  17181  setsexstruct2  17183  pwsvscaval  17497  2initoinv  18015  initoeu1  18016  initoeu2lem1  18019  initoeu2  18021  2termoinv  18022  termoeu1  18023  homarel  18041  joinfval  18375  meetfval  18389  latjcom  18451  latmcom  18467  0subm  18823  sgrp2nmndlem5  18938  grprcan  18987  isgrpid2  18990  grpinvid  19013  mulgnn0z  19115  qus0  19202  eqg0subg  19209  ghmker  19254  symgbasmap  19389  symginv  19414  pmtrfrn  19470  odmulg2  19567  slwpgp  19625  pj1eq  19712  efgtf  19734  frgpinv  19776  frgpup2  19788  cnaddablx  19880  cnaddabl  19881  zaddablx  19884  imasabl  19888  dprdfadd  20034  dpjidcl  20072  dpjlid  20075  pgpfac1lem3  20091  omndmul2  20145  omndmul  20147  srgen1zr  20234  1unit  20391  unitgrpid  20402  1rinv  20412  irredn0  20440  irredneg  20447  c0snmgmhm  20479  rngisomring1  20485  zrrnghm  20554  rnrhmsubrg  20623  zrinitorngc  20660  zrtermorngc  20661  zrtermoringc  20693  isdrng2  20761  ringen1zr  20796  abv0  20841  abv1z  20842  abvneg  20844  orng0le1  20892  lmodfopne  20936  lsssn0  20984  lspsn0  21044  lsp0  21045  lmhmvsca  21081  lmhmrnlss  21086  lmhmkerlss  21087  lsppratlem5  21190  rsp1  21276  kerlidl  21317  ring2idlqus  21348  rngqiprngfulem4  21353  rngqiprngfu  21356  cnfldneg  21419  zringcyg  21490  chrid  21546  chrrhm  21552  ip0r  21658  ocvlss  21693  ocv1  21700  rlmassa  21891  psrbagfsupp  21940  snifpsrbag  21941  psrbaglefi  21947  psrvscaval  21971  psrdi  21985  psrdir  21986  mplvscaval  22036  mhpmpl  22178  mhpdeg  22179  mhppwdeg  22184  psdmul  22200  psdpw  22204  coe1sclmulfv  22315  coe1id  22325  ply1idvr1OLD  22327  evl1var  22368  mamuvs1  22434  mamuvs2  22435  matecl  22454  matvscacell  22465  mat0scmat  22567  submaval0  22609  mdetrsca  22632  maduval  22667  minmar1val0  22676  pmatcollpw3fi1lem2  22816  chcoeffeqlem  22914  cayleyhamilton0  22918  cayleyhamiltonALT  22920  toponsspwpw  22951  cctop  23035  cldval  23052  ntrfval  23053  clsfval  23054  cmclsopn  23091  opncldf3  23115  neifval  23128  lpfval  23167  cnrmnrm  23390  dis2ndc  23489  islocfin  23546  tx1cn  23638  idqtop  23735  kqtopon  23756  kqid  23757  kqcld  23764  hmphen2  23828  filssufil  23941  ufileu  23948  alexsublem  24073  efmndtmd  24130  symgtgp  24135  ustuqtop4  24273  cstucnd  24312  metustexhalf  24585  nm0  24658  rlmnlm  24717  nmolb  24746  metdseq0  24884  pi1xfrval  25085  clmvneg1  25130  clmvsubval  25140  ipcau2  25265  tcphcphlem1  25266  tcphcphlem2  25267  cmetcaulem  25319  ovolicc2lem3  25550  ovolicc2lem4  25551  mbfmulc2lem  25678  i1fpos  25737  mbfi1fseqlem3  25748  itg2ge0  25766  bddiblnc  25873  dvres2  25943  dvaddbr  25969  dvmulbr  25970  dvcobr  25977  dvfsumlem4  26060  ftc1a  26068  ftc1lem6  26072  uc1pmon1p  26181  ig1pval2  26206  dgradd2  26297  dgrcolem2  26303  plydivlem4  26326  plydiveu  26328  elqaalem3  26351  qaa  26353  ulmdvlem1  26429  abelthlem6  26465  abelthlem7  26467  eflogeq  26633  jensenlem2  27018  harmonicbnd4  27041  sgmnncl  27177  dchrptlem2  27295  1lgs  27370  lgs1  27371  2sqcoprm  27465  addsqnreup  27473  dchrisumlem2  27520  dchrisum0lem2a  27547  selberg2lem  27580  pntrsumo1  27595  pntrsumbnd  27596  pntpbnd1  27616  pntlemr  27632  pntlemj  27633  padicabvf  27661  bdayval  27678  noextendgt  27700  nosupbnd2lem1  27745  noinfbnd2lem1  27760  noetainflem4  27770  oldval  27893  divmuls  28280  divscl  28282  seqsp1  28370  bdayfinbndlem1  28526  zz12s  28534  remulscllem1  28559  incistruhgr  29215  subgrprop3  29412  subgruhgredgd  29420  usgrexi  29577  cusgrexi  29579  cusgrsizeinds  29588  vtxdgfusgrf  29633  1hevtxdg1  29642  1egrvtxdg1  29645  ewlkprop  29739  wlklenvm1  29757  wlkl1loop  29773  wlkp1lem4  29810  2pthnloop  29866  upgrclwlkcompim  29916  crctcshwlkn0lem4  29948  crctcshwlkn0lem5  29949  crctcshwlkn0lem6  29950  crctcshwlkn0lem7  29951  crctcshlem4  29955  wspthnonp  29994  wlkswwlksf1o  30014  wwlksnwwlksnon  30050  umgr2wlkon  30085  wwlks2onv  30088  elwwlks2ons3im  30089  elwspths2spth  30105  umgrclwwlkge2  30128  clwlkclwwlkf1lem3  30143  erclwwlkref  30157  clwwlknp  30174  wwlksext2clwwlk  30194  wwlksubclwwlk  30195  0pthon1  30265  1wlkdlem4  30277  1pthd  30280  3spthd  30313  eupth2eucrct  30354  eucrctshift  30380  eucrct2eupth  30382  frgrncvvdeqlem8  30443  frgr2wwlkeqm  30468  isgrpoi  30636  grpoinvfval  30660  grpodivfval  30672  vcz  30713  cnaddabloOLD  30719  nvz0  30806  sspz  30873  lno0  30894  nmobndi  30913  ipasslem2  30970  shunssi  31506  ococin  31546  ssjo  31585  pjocini  31836  nlfnval  32019  lncnopbd  32175  riesz3i  32200  cnlnadjlem7  32211  pjclem4  32337  pj3si  32345  hstoc  32360  hstnmoc  32361  hstoh  32370  hst0  32371  mdsl2i  32460  chirredlem3  32530  chirredlem4  32531  dmdbr5ati  32560  rexunirn  32628  fcnvgreu  32813  infxrge0glb  32906  sgnneg  32974  cycpmco2lem5  33260  cycpmco2lem6  33261  cycpmco2lem7  33262  isarchi3  33317  nsgqusf1olem2  33546  ssdifidllem  33588  ssmxidllem  33605  rprmdvdspow  33673  ressply1sub  33710  selvply1rhmlemb  33760  fedgmullem1  33870  extdg1id  33907  nn0constr  34002  zartopn  34116  zarcmplem  34122  esumcvg  34327  esumcvgre  34332  sigaval  34352  unelldsys  34399  fiunelros  34415  measval  34439  pmeasmono  34565  probfinmeasb  34669  ballotlemfc0  34734  ballotlemfcc  34735  ballotlemsi  34756  ballotlemfrci  34769  signlem0  34828  breprexp  34874  bnj1006  35202  bnj1110  35224  bnj1253  35259  bnj1280  35262  bnj1463  35297  bnj1312  35300  fineqvinfep  35366  erdszelem7  35485  erdszelem8  35486  cvmliftlem10  35582  cvmliftlem13  35584  cvmlift2lem9  35599  cvmlift3lem6  35612  cvmlift3lem7  35613  cvmlift3lem9  35615  satfv1lem  35650  dfrdg2  36081  cldregopn  36629  tailfval  36670  filnetlem3  36678  filnetlem4  36679  ontopbas  36726  bj-nnfbd  37182  bj-elid4  37598  bj-imdiridlem  37615  f1omptsnlem  37768  icoreunrn  37791  relowlpssretop  37796  fvineqsnf1  37842  wl-sbal2  38005  unccur  38040  poimirlem1  38058  poimirlem2  38059  poimirlem4  38061  poimirlem6  38063  poimirlem7  38064  poimirlem11  38068  poimirlem12  38069  poimirlem17  38074  poimirlem20  38077  poimirlem22  38079  poimirlem23  38080  poimirlem28  38085  poimir  38090  ismblfin  38098  cnambfre  38105  ftc1cnnc  38129  dvasin  38141  ismtyres  38245  heiborlem8  38255  ghomidOLD  38326  rngosn6  38363  rngonegmn1l  38378  rngonegmn1r  38379  rngoneglmul  38380  rngonegrmul  38381  idlnegcl  38459  0idl  38462  0rngo  38464  smprngopr  38489  sucmapsuc  38926  cossex  38946  qsdisjALTV  39136  cnvepresdmqss  39174  mpets2  39392  lkrval  39650  ldualvaddval  39693  ldualvsval  39700  opoc1  39764  pmap0  40327  pmap1N  40329  pexmidALTN  40540  cdleme31fv  40952  cdlemg27b  41258  erngdvlem4  41553  erng0g  41556  erngdvlem4-rN  41561  dvalveclem  41587  dvh0g  41673  dih0cnv  41845  dih1rn  41849  dih1cnv  41850  doch0  41920  doch1  41921  lcfl7lem  42061  mapdheq  42290  hdmap1eq  42363  hdmapval2lem  42393  hgmapvvlem3  42487  zndvdchrrhm  42528  lcmineqlem13  42596  aks4d1p9  42643  primrootsunit1  42652  aks6d1c1p1  42662  aks6d1c1p6  42669  aks6d1c1p8  42670  sticksstones1  42701  sticksstones6  42706  sticksstones7  42707  sticksstones11  42711  sticksstones12a  42712  sticksstones12  42713  sticksstones22  42723  aks6d1c6isolem1  42729  aks6d1c6isolem2  42730  unitscyglem5  42754  renegid  42920  sn-0ne2  42953  remul01  42954  remulinvcom  42980  sn-0tie0  43011  renegmulnnass  43025  domnexpgn0cl  43079  abvexp  43088  frlmsnic  43096  fsuppssind  43113  mzpval  43251  mzpindd  43265  pellex  43350  2nn0ind  43460  jm2.26lem3  43516  pw2f1o2val  43554  wepwsolem  43557  fnwe2lem3  43567  lnmfg  43597  dgrsub2  43650  mpaaeu  43665  flcidc  43685  dflim5  43844  naddwordnexlem1  43912  rtrclexlem  44130  cnvrcl0  44139  brcoffn  44544  clsk1indlem3  44557  clsneif1o  44618  clsneicnv  44619  clsneikex  44620  clsneinex  44621  neicvgmex  44631  neicvgel1  44633  suprleubrd  44680  suprlubrd  44682  imo72b2  44686  dvconstbi  44848  bcc0  44854  binomcxplemnotnn0  44870  nnfoctb  45566  infleinflem1  45883  fprodcnlem  46113  sumnnodd  46144  icccncfext  46399  itgsin0pilem1  46462  stoweidlem32  46544  stoweidlem35  46547  stoweidlem36  46548  stoweidlem37  46549  stoweidlem43  46555  stoweidlem50  46562  wallispilem5  46581  stirlinglem2  46587  stirlinglem3  46588  stirlinglem4  46589  stirlinglem8  46593  stirlinglem11  46596  stirlinglem12  46597  stirlinglem14  46599  stirlinglem15  46600  fourierdlem11  46630  fourierdlem20  46639  fourierdlem21  46640  fourierdlem41  46660  fourierdlem42  46661  fourierdlem48  46666  fourierdlem49  46667  fourierdlem64  46682  fourierdlem71  46689  fourierdlem79  46697  fourierdlem90  46708  fourierdlem91  46709  fourierswlem  46742  etransclem17  46763  etransclem38  46784  saluni  46837  meaiininclem  46998  issmflelem  47256  issmfgtlem  47267  issmfgelem  47281  smflimsuplem4  47335  f1cof1blem  47606  zplusmodne  47881  m1modne  47886  submodneaddmod  47889  nndivides2  47916  sprval  48023  prprval  48058  bgoldbtbndlem2  48366  bgoldbtbndlem3  48367  bgoldbtbnd  48369  isubgrvtxuhgr  48424  isubgredg  48426  grimcnv  48448  isuspgrim  48456  gricushgr  48477  uhgrimisgrgric  48491  grtriclwlk3  48505  isubgr3stgrlem7  48532  grlimgrtri  48563  grlictr  48575  gpgvtx0  48613  gpgvtx1  48614  gpgprismgrusgra  48618  gpgedgvtx1  48622  gpg3kgrtriex  48649  pgnbgreunbgrlem3  48678  pgnbgreunbgrlem6  48684  isclintop  48767  clintopcllaw  48771  nzrneg1ne0  48790  lidldomn1  48791  zlidlring  48794  uzlidlring  48795  2zrngnmlid  48815  cznrng  48821  blenre  49134  blennn  49135  2arymaptf  49212  itcoval1  49223  itcovalendof  49229  ehl2eudisval0  49285  eenglngeehlnmlem2  49298  itsclc0yqsol  49324  inlinecirc02plem  49346  ipolub  49547  ipoglb  49550  nelsubclem  49626  imaid  49713  imaf1co  49714  uptri  49773  uptrar  49775  uptrai  49776  oppc1stflem  49846  setrec2mpt  50256