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  2978  csbiegf  3170  difsnb  3817  reusv3i  4558  fimadmfo  5571  fvmpt3  5728  ffvelcdmd  5786  fnressn  5843  fliftel1  5940  f1oiso2  5973  riota5f  6003  1stvalg  6310  2ndvalg  6311  brtpos2  6422  tfrlemibxssdm  6498  dom2lem  6950  php5  7049  nnfi  7064  xpfi  7129  supisoti  7214  ordiso2  7239  omp1eomlem  7298  nnnninfeq2  7333  onenon  7393  oncardval  7395  cardonle  7396  recidnq  7618  archnqq  7642  prarloclemarch2  7644  recexprlem1ssl  7858  recexprlem1ssu  7859  recexprlemss1l  7860  recexprlemss1u  7861  recexprlemex  7862  0idsr  7992  lep1  9030  suprlubex  9137  uz11  9784  xnegid  10099  eluzfz2  10272  fzsuc  10309  fzsuc2  10319  fzp1disj  10320  fzneuz  10341  fzp1nel  10344  nn0p1elfzo  10427  exbtwnzlemex  10515  flhalf  10568  modqval  10592  frec2uzsucd  10669  frecuzrdgsuc  10682  uzsinds  10712  seq3p1  10733  seqp1cd  10738  expubnd  10864  iexpcyc  10912  binom2sub1  10922  hashennn  11048  lswwrd  11169  eqs1  11214  pfxid  11276  wrdind  11312  wrd2ind  11313  pfxccatpfx2  11327  swrdccat3blem  11329  shftfval  11404  shftcan1  11417  cjval  11428  reval  11432  imval  11433  cjmulrcl  11470  addcj  11474  absval  11584  resqrexlemdecn  11595  resqrexlemnmsq  11600  resqrexlemnm  11601  absneg  11633  abscj  11635  sqabsadd  11638  sqabssub  11639  ltabs  11670  dfabsmax  11800  negfi  11811  fsum3  11971  trirecip  12085  fprodseq  12167  efval  12245  ege2le3  12255  efcan  12260  sinval  12286  cosval  12287  efi4p  12301  resin4p  12302  recos4p  12303  sincossq  12332  eirraplem  12361  iddvds  12388  1dvds  12389  bezoutlemstep  12591  coprmgcdb  12683  1idssfct  12710  exprmfct  12733  oddpwdclemdc  12768  phival  12808  odzphi  12842  oddprmdvds  12950  setsn0fun  13142  gsumfzval  13497  0subm  13590  gsumfzz  13601  grprcan  13643  isgrpid2  13646  grpinvid  13666  mulgval  13732  mulgnn0z  13759  0subg  13809  qus0  13845  ghmker  13880  imasabl  13946  mgpplusgg  13961  mgpbasg  13963  mgpscag  13964  mgptsetg  13965  mgpdsg  13967  srgen1zr  14025  opprmulfvalg  14107  opprsllem  14111  1unit  14145  1rinv  14166  subrngmcl  14247  subrg1  14269  subrgmcl  14271  subrgdvds  14273  subrguss  14274  subrginv  14275  subrgdv  14276  subrgunit  14277  subrgugrp  14278  rnrhmsubrg  14290  lmodfopne  14364  lsssn0  14408  lspsn0  14460  lsp0  14461  sralmod  14488  2idlval  14540  cnfldneg  14611  zrhval  14655  cldval  14852  ntrfval  14853  clsfval  14854  neifval  14893  tx1cn  15022  ismet  15097  isxmet  15098  divcnap  15318  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  sgmnncl  15741  1lgs  15801  lgs1  15802  uhgredgiedgb  16014  uhgriedg0edg0  16015  subgrprop3  16142  wlklenvm1  16221  wlklenvm1g  16222  wlkl1loop  16238  wlklenvclwlk  16253  umgrclwwlkge2  16282  clwwlknp  16297  bj-charfun  16462  bj-findis  16634