Theorem mpdan 425

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 19	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpidan  427  mpan2  429  biadanid  622  mpjaodan  810  mpd3an3  1379  eueq2dc  2999  csbiegf  3191  difsnb  3858  reusv3i  4605  fimadmfo  5624  fvmpt3  5784  ffvelcdmd  5844  fnressn  5901  fliftel1  6000  f1oiso2  6033  riota5f  6065  1stvalg  6376  2ndvalg  6377  brtpos2  6522  tfrlemibxssdm  6598  dom2lem  7058  php5  7159  nnfi  7174  xpfi  7239  supisoti  7350  ordiso2  7375  omp1eomlem  7434  nnnninfeq2  7469  onenon  7529  oncardval  7531  cardonle  7532  recidnq  7760  archnqq  7784  prarloclemarch2  7786  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  recexprlemex  8004  0idsr  8134  lep1  9177  suprlubex  9284  uz11  9954  xnegid  10271  eluzfz2  10446  fzsuc  10485  fzsuc2  10496  fzp1disj  10497  fzneuz  10518  fzp1nel  10521  nn0p1elfzo  10604  exbtwnzlemex  10694  flhalf  10750  modqval  10774  frec2uzsucd  10851  frecuzrdgsuc  10864  uzsinds  10894  seq3p1  10915  seqp1cd  10920  expubnd  11046  iexpcyc  11094  binom2sub1  11104  hashennn  11233  lswwrd  11365  eqs1  11410  pfxid  11472  wrdind  11508  wrd2ind  11509  pfxccatpfx2  11523  swrdccat3blem  11525  shftfval  11600  shftcan1  11613  cjval  11624  reval  11628  imval  11629  cjmulrcl  11666  addcj  11670  absval  11781  resqrexlemdecn  11792  resqrexlemnmsq  11797  resqrexlemnm  11798  absneg  11830  abscj  11832  sqabsadd  11835  sqabssub  11836  ltabs  11868  dfabsmax  11998  negfi  12009  fsum3  12170  trirecip  12284  fprodseq  12366  efval  12444  ege2le3  12454  efcan  12459  sinval  12485  cosval  12486  efi4p  12500  resin4p  12501  recos4p  12502  sincossq  12531  eirraplem  12560  iddvds  12587  1dvds  12588  bezoutlemstep  12790  coprmgcdb  12882  1idssfct  12909  exprmfct  12933  pwbdvdslemn  12960  phival  13011  odzphi  13045  oddprmdvds  13153  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsi  13307  ballotfilemfrci  13320  setsn0fun  13438  gzsumfzval  13760  0subm  13840  grprcan  13891  isgrpid2  13894  grpinvid  13914  mulgval  13974  mulgnn0z  14001  0subg  14051  qus0  14087  ghmker  14122  imasabl  14189  mgpplusgg  14270  mgpbasg  14273  mgpscag  14275  mgptsetg  14276  mgpdsg  14278  rngen1zr0  14310  srgen1zr0  14341  opprmulfvalg  14424  opprsllem  14428  1unit  14463  1rinv  14484  subrngmcl  14566  subrg1  14588  subrgmcl  14590  subrgdvds  14592  subrguss  14593  subrginv  14594  subrgdv  14595  subrgunit  14596  subrgugrp  14597  rnrhmsubrg  14609  lmodfopne  14712  lsssn0  14756  lspsn0  14808  lsp0  14809  sralmod  14836  2idlval  14888  cnfldneg  14959  zrhval  15001  psrbagfsupp  15104  cldval  15249  ntrfval  15250  clsfval  15251  neifval  15290  tx1cn  15419  ismet  15494  isxmet  15495  divcnap  15715  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  sgmnncl  16176  1lgs  16281  lgs1  16282  uhgredgiedgb  16494  uhgriedg0edg0  16495  subgrprop3  16622  wlklenvm1  16701  wlklenvm1g  16702  wlkl1loop  16718  wlklenvclwlk  16733  umgrclwwlkge2  16762  clwwlknp  16777  bj-charfun  16952  bj-findis  17124