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  806  mpd3an3  1375  eueq2dc  2989  csbiegf  3181  difsnb  3836  reusv3i  4579  fimadmfo  5598  fvmpt3  5755  ffvelcdmd  5812  fnressn  5869  fliftel1  5966  f1oiso2  5999  riota5f  6029  1stvalg  6335  2ndvalg  6336  brtpos2  6481  tfrlemibxssdm  6557  dom2lem  7010  php5  7111  nnfi  7126  xpfi  7191  supisoti  7300  ordiso2  7325  omp1eomlem  7384  nnnninfeq2  7419  onenon  7479  oncardval  7481  cardonle  7482  recidnq  7704  archnqq  7728  prarloclemarch2  7730  recexprlem1ssl  7944  recexprlem1ssu  7945  recexprlemss1l  7946  recexprlemss1u  7947  recexprlemex  7948  0idsr  8078  lep1  9115  suprlubex  9222  uz11  9873  xnegid  10188  eluzfz2  10362  fzsuc  10399  fzsuc2  10409  fzp1disj  10410  fzneuz  10431  fzp1nel  10434  nn0p1elfzo  10517  exbtwnzlemex  10605  flhalf  10658  modqval  10682  frec2uzsucd  10759  frecuzrdgsuc  10772  uzsinds  10802  seq3p1  10823  seqp1cd  10828  expubnd  10954  iexpcyc  11002  binom2sub1  11012  hashennn  11138  lswwrd  11264  eqs1  11309  pfxid  11371  wrdind  11407  wrd2ind  11408  pfxccatpfx2  11422  swrdccat3blem  11424  shftfval  11499  shftcan1  11512  cjval  11523  reval  11527  imval  11528  cjmulrcl  11565  addcj  11569  absval  11679  resqrexlemdecn  11690  resqrexlemnmsq  11695  resqrexlemnm  11696  absneg  11728  abscj  11730  sqabsadd  11733  sqabssub  11734  ltabs  11765  dfabsmax  11895  negfi  11906  fsum3  12066  trirecip  12180  fprodseq  12262  efval  12340  ege2le3  12350  efcan  12355  sinval  12381  cosval  12382  efi4p  12396  resin4p  12397  recos4p  12398  sincossq  12427  eirraplem  12456  iddvds  12483  1dvds  12484  bezoutlemstep  12686  coprmgcdb  12778  1idssfct  12805  exprmfct  12828  oddpwdclemdc  12863  phival  12903  odzphi  12937  oddprmdvds  13045  setsn0fun  13238  gsumfzval  13593  0subm  13686  gsumfzz  13697  grprcan  13739  isgrpid2  13742  grpinvid  13762  mulgval  13828  mulgnn0z  13855  0subg  13905  qus0  13941  ghmker  13976  imasabl  14042  mgpplusgg  14057  mgpbasg  14059  mgpscag  14060  mgptsetg  14061  mgpdsg  14063  srgen1zr  14121  opprmulfvalg  14203  opprsllem  14207  1unit  14241  1rinv  14262  subrngmcl  14343  subrg1  14365  subrgmcl  14367  subrgdvds  14369  subrguss  14370  subrginv  14371  subrgdv  14372  subrgunit  14373  subrgugrp  14374  rnrhmsubrg  14386  lmodfopne  14461  lsssn0  14505  lspsn0  14557  lsp0  14558  sralmod  14585  2idlval  14637  cnfldneg  14708  zrhval  14752  psrbagfsupp  14806  cldval  14951  ntrfval  14952  clsfval  14953  neifval  14992  tx1cn  15121  ismet  15196  isxmet  15197  divcnap  15417  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  sgmnncl  15843  1lgs  15903  lgs1  15904  uhgredgiedgb  16116  uhgriedg0edg0  16117  subgrprop3  16244  wlklenvm1  16323  wlklenvm1g  16324  wlkl1loop  16340  wlklenvclwlk  16355  umgrclwwlkge2  16384  clwwlknp  16399  bj-charfun  16564  bj-findis  16736