Theorem mpdan 421

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpidan  423  mpan2  425  biadanid  618  mpjaodan  805  mpd3an3  1374  eueq2dc  2979  csbiegf  3171  difsnb  3816  reusv3i  4556  fimadmfo  5568  fvmpt3  5725  ffvelcdmd  5783  fnressn  5840  fliftel1  5935  f1oiso2  5968  riota5f  5998  1stvalg  6305  2ndvalg  6306  brtpos2  6417  tfrlemibxssdm  6493  dom2lem  6945  php5  7044  nnfi  7059  xpfi  7124  supisoti  7209  ordiso2  7234  omp1eomlem  7293  nnnninfeq2  7328  onenon  7388  oncardval  7390  cardonle  7391  recidnq  7613  archnqq  7637  prarloclemarch2  7639  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  recexprlemex  7857  0idsr  7987  lep1  9025  suprlubex  9132  uz11  9779  xnegid  10094  eluzfz2  10267  fzsuc  10304  fzsuc2  10314  fzp1disj  10315  fzneuz  10336  fzp1nel  10339  nn0p1elfzo  10422  exbtwnzlemex  10510  flhalf  10563  modqval  10587  frec2uzsucd  10664  frecuzrdgsuc  10677  uzsinds  10707  seq3p1  10728  seqp1cd  10733  expubnd  10859  iexpcyc  10907  binom2sub1  10917  hashennn  11043  lswwrd  11161  eqs1  11206  pfxid  11268  wrdind  11304  wrd2ind  11305  pfxccatpfx2  11319  swrdccat3blem  11321  shftfval  11383  shftcan1  11396  cjval  11407  reval  11411  imval  11412  cjmulrcl  11449  addcj  11453  absval  11563  resqrexlemdecn  11574  resqrexlemnmsq  11579  resqrexlemnm  11580  absneg  11612  abscj  11614  sqabsadd  11617  sqabssub  11618  ltabs  11649  dfabsmax  11779  negfi  11790  fsum3  11950  trirecip  12064  fprodseq  12146  efval  12224  ege2le3  12234  efcan  12239  sinval  12265  cosval  12266  efi4p  12280  resin4p  12281  recos4p  12282  sincossq  12311  eirraplem  12340  iddvds  12367  1dvds  12368  bezoutlemstep  12570  coprmgcdb  12662  1idssfct  12689  exprmfct  12712  oddpwdclemdc  12747  phival  12787  odzphi  12821  oddprmdvds  12929  setsn0fun  13121  gsumfzval  13476  0subm  13569  gsumfzz  13580  grprcan  13622  isgrpid2  13625  grpinvid  13645  mulgval  13711  mulgnn0z  13738  0subg  13788  qus0  13824  ghmker  13859  imasabl  13925  mgpplusgg  13940  mgpbasg  13942  mgpscag  13943  mgptsetg  13944  mgpdsg  13946  srgen1zr  14004  opprmulfvalg  14086  opprsllem  14090  1unit  14124  1rinv  14145  subrngmcl  14226  subrg1  14248  subrgmcl  14250  subrgdvds  14252  subrguss  14253  subrginv  14254  subrgdv  14255  subrgunit  14256  subrgugrp  14257  rnrhmsubrg  14269  lmodfopne  14343  lsssn0  14387  lspsn0  14439  lsp0  14440  sralmod  14467  2idlval  14519  cnfldneg  14590  zrhval  14634  cldval  14826  ntrfval  14827  clsfval  14828  neifval  14867  tx1cn  14996  ismet  15071  isxmet  15072  divcnap  15292  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  sgmnncl  15715  1lgs  15775  lgs1  15776  uhgredgiedgb  15988  uhgriedg0edg0  15989  subgrprop3  16116  wlklenvm1  16195  wlklenvm1g  16196  wlkl1loop  16212  wlklenvclwlk  16227  umgrclwwlkge2  16256  clwwlknp  16271  bj-charfun  16423  bj-findis  16595