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  7351  ordiso2  7376  omp1eomlem  7435  nnnninfeq2  7470  onenon  7530  oncardval  7532  cardonle  7533  recidnq  7761  archnqq  7785  prarloclemarch2  7787  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  recexprlemex  8005  0idsr  8135  lep1  9178  suprlubex  9285  uz11  9955  xnegid  10272  eluzfz2  10447  fzsuc  10486  fzsuc2  10497  fzp1disj  10498  fzneuz  10519  fzp1nel  10522  nn0p1elfzo  10605  exbtwnzlemex  10695  flhalf  10752  modqval  10776  frec2uzsucd  10853  frecuzrdgsuc  10866  uzsinds  10896  seq3p1  10917  seqp1cd  10922  expubnd  11048  iexpcyc  11096  binom2sub1  11106  hashennn  11235  lswwrd  11367  eqs1  11412  pfxid  11474  wrdind  11510  wrd2ind  11511  pfxccatpfx2  11525  swrdccat3blem  11527  shftfval  11602  shftcan1  11615  cjval  11626  reval  11630  imval  11631  cjmulrcl  11668  addcj  11672  absval  11783  resqrexlemdecn  11794  resqrexlemnmsq  11799  resqrexlemnm  11800  absneg  11832  abscj  11834  sqabsadd  11837  sqabssub  11838  ltabs  11870  dfabsmax  12000  negfi  12011  fsum3  12173  trirecip  12287  fprodseq  12369  efval  12447  ege2le3  12457  efcan  12462  sinval  12488  cosval  12489  efi4p  12503  resin4p  12504  recos4p  12505  sincossq  12534  eirraplem  12563  iddvds  12590  1dvds  12591  bezoutlemstep  12793  coprmgcdb  12885  1idssfct  12912  exprmfct  12936  pwbdvdslemn  12963  phival  13014  odzphi  13048  oddprmdvds  13156  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsi  13310  ballotfilemfrci  13323  setsn0fun  13441  gzsumfzval  13764  0subm  13844  grprcan  13895  isgrpid2  13898  grpinvid  13918  mulgval  13978  mulgnn0z  14005  0subg  14055  qus0  14091  ghmker  14126  imasabl  14224  mgpplusgg  14305  mgpbasg  14308  mgpscag  14310  mgptsetg  14311  mgpdsg  14313  rngen1zr0  14345  srgen1zr0  14376  opprmulfvalg  14459  opprsllem  14463  1unit  14498  1rinv  14519  subrngmcl  14601  subrg1  14623  subrgmcl  14625  subrgdvds  14627  subrguss  14628  subrginv  14629  subrgdv  14630  subrgunit  14631  subrgugrp  14632  rnrhmsubrg  14644  lmodfopne  14747  lsssn0  14791  lspsn0  14843  lsp0  14844  sralmod  14871  2idlval  14923  cnfldneg  14994  zrhval  15036  psrbagfsupp  15139  cldval  15291  ntrfval  15292  clsfval  15293  neifval  15332  tx1cn  15461  ismet  15536  isxmet  15537  divcnap  15757  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  sgmnncl  16223  1lgs  16333  lgs1  16334  uhgredgiedgb  16546  uhgriedg0edg0  16547  subgrprop3  16674  wlklenvm1  16753  wlklenvm1g  16754  wlkl1loop  16770  wlklenvclwlk  16785  umgrclwwlkge2  16814  clwwlknp  16829  bj-charfun  17004  bj-findis  17176