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  616  mpjaodan  803  mpd3an3  1372  eueq2dc  2976  csbiegf  3168  difsnb  3811  reusv3i  4551  fimadmfo  5562  fvmpt3  5718  ffvelcdmd  5776  fnressn  5832  fliftel1  5927  f1oiso2  5960  riota5f  5990  1stvalg  6297  2ndvalg  6298  brtpos2  6408  tfrlemibxssdm  6484  dom2lem  6936  php5  7032  nnfi  7047  xpfi  7110  supisoti  7193  ordiso2  7218  omp1eomlem  7277  nnnninfeq2  7312  onenon  7372  oncardval  7374  cardonle  7375  recidnq  7596  archnqq  7620  prarloclemarch2  7622  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  recexprlemex  7840  0idsr  7970  lep1  9008  suprlubex  9115  uz11  9762  xnegid  10072  eluzfz2  10245  fzsuc  10282  fzsuc2  10292  fzp1disj  10293  fzneuz  10314  fzp1nel  10317  exbtwnzlemex  10486  flhalf  10539  modqval  10563  frec2uzsucd  10640  frecuzrdgsuc  10653  uzsinds  10683  seq3p1  10704  seqp1cd  10709  expubnd  10835  iexpcyc  10883  binom2sub1  10893  hashennn  11019  lswwrd  11136  eqs1  11181  pfxid  11239  wrdind  11275  wrd2ind  11276  pfxccatpfx2  11290  swrdccat3blem  11292  shftfval  11353  shftcan1  11366  cjval  11377  reval  11381  imval  11382  cjmulrcl  11419  addcj  11423  absval  11533  resqrexlemdecn  11544  resqrexlemnmsq  11549  resqrexlemnm  11550  absneg  11582  abscj  11584  sqabsadd  11587  sqabssub  11588  ltabs  11619  dfabsmax  11749  negfi  11760  fsum3  11919  trirecip  12033  fprodseq  12115  efval  12193  ege2le3  12203  efcan  12208  sinval  12234  cosval  12235  efi4p  12249  resin4p  12250  recos4p  12251  sincossq  12280  eirraplem  12309  iddvds  12336  1dvds  12337  bezoutlemstep  12539  coprmgcdb  12631  1idssfct  12658  exprmfct  12681  oddpwdclemdc  12716  phival  12756  odzphi  12790  oddprmdvds  12898  setsn0fun  13090  gsumfzval  13445  0subm  13538  gsumfzz  13549  grprcan  13591  isgrpid2  13594  grpinvid  13614  mulgval  13680  mulgnn0z  13707  0subg  13757  qus0  13793  ghmker  13828  imasabl  13894  mgpplusgg  13908  mgpbasg  13910  mgpscag  13911  mgptsetg  13912  mgpdsg  13914  srgen1zr  13972  opprmulfvalg  14054  opprsllem  14058  1unit  14092  1rinv  14113  subrngmcl  14194  subrg1  14216  subrgmcl  14218  subrgdvds  14220  subrguss  14221  subrginv  14222  subrgdv  14223  subrgunit  14224  subrgugrp  14225  rnrhmsubrg  14237  lmodfopne  14311  lsssn0  14355  lspsn0  14407  lsp0  14408  sralmod  14435  2idlval  14487  cnfldneg  14558  zrhval  14602  cldval  14794  ntrfval  14795  clsfval  14796  neifval  14835  tx1cn  14964  ismet  15039  isxmet  15040  divcnap  15260  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  sgmnncl  15683  1lgs  15743  lgs1  15744  uhgredgiedgb  15953  uhgriedg0edg0  15954  wlklenvm1  16113  wlklenvm1g  16114  wlkl1loop  16130  wlklenvclwlk  16145  umgrclwwlkge2  16171  clwwlknp  16185  bj-charfun  16279  bj-findis  16451