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  4607  fimadmfo  5627  fvmpt3  5787  ffvelcdmd  5847  fnressn  5904  fliftel1  6003  f1oiso2  6036  riota5f  6068  1stvalg  6380  2ndvalg  6381  brtpos2  6526  tfrlemibxssdm  6602  dom2lem  7063  php5  7164  nnfi  7179  xpfi  7244  supisoti  7357  ordiso2  7382  omp1eomlem  7441  nnnninfeq2  7476  onenon  7536  oncardval  7538  cardonle  7539  recidnq  7767  archnqq  7791  prarloclemarch2  7793  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  recexprlemex  8011  0idsr  8141  lep1  9184  suprlubex  9291  uz11  9962  xnegid  10279  eluzfz2  10454  fzsuc  10493  fzsuc2  10504  fzp1disj  10505  fzneuz  10526  fzp1nel  10529  nn0p1elfzo  10612  exbtwnzlemex  10702  flhalf  10759  modqval  10783  frec2uzsucd  10860  frecuzrdgsuc  10873  uzsinds  10903  seq3p1  10924  seqp1cd  10929  expubnd  11055  iexpcyc  11103  binom2sub1  11113  hashennn  11242  lswwrd  11374  eqs1  11419  pfxid  11481  wrdind  11517  wrd2ind  11518  pfxccatpfx2  11532  swrdccat3blem  11534  shftfval  11609  shftcan1  11622  cjval  11633  reval  11637  imval  11638  cjmulrcl  11675  addcj  11679  absval  11790  resqrexlemdecn  11801  resqrexlemnmsq  11806  resqrexlemnm  11807  absneg  11839  abscj  11841  sqabsadd  11844  sqabssub  11845  ltabs  11877  dfabsmax  12007  negfi  12018  fsum3  12180  trirecip  12294  fprodseq  12376  efval  12454  ege2le3  12464  efcan  12469  sinval  12495  cosval  12496  efi4p  12510  resin4p  12511  recos4p  12512  sincossq  12541  eirraplem  12570  iddvds  12597  1dvds  12598  bezoutlemstep  12800  coprmgcdb  12892  1idssfct  12919  exprmfct  12943  pwbdvdslemn  12970  phival  13021  odzphi  13055  oddprmdvds  13163  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemsi  13317  ballotfilemfrci  13330  setsn0fun  13448  gzsumfzval  13771  0subm  13851  grprcan  13902  isgrpid2  13905  grpinvid  13925  mulgval  13985  mulgnn0z  14012  0subg  14062  qus0  14098  ghmker  14133  imasabl  14231  mgpplusgg  14329  mgpbasg  14332  mgpscag  14334  mgptsetg  14335  mgpdsg  14337  rngen1zr0  14369  srgen1zr0  14400  opprmulfvalg  14485  opprsllem  14489  1unit  14524  1rinv  14545  subrngmcl  14627  subrg1  14649  subrgmcl  14651  subrgdvds  14653  subrguss  14654  subrginv  14655  subrgdv  14656  subrgunit  14657  subrgugrp  14658  rnrhmsubrg  14670  lmodfopne  14773  lsssn0  14817  lspsn0  14869  lsp0  14870  sralmod  14897  2idlval  14949  cnfldneg  15020  zrhval  15062  psrbagfsupp  15167  psrdifi  15207  psrdirfi  15208  cldval  15337  ntrfval  15338  clsfval  15339  neifval  15378  tx1cn  15507  ismet  15582  isxmet  15583  divcnap  15803  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  sgmnncl  16269  1lgs  16379  lgs1  16380  uhgredgiedgb  16592  uhgriedg0edg0  16593  subgrprop3  16720  wlklenvm1  16799  wlklenvm1g  16800  wlkl1loop  16816  wlklenvclwlk  16831  umgrclwwlkge2  16860  clwwlknp  16875  bj-charfun  17050  bj-findis  17222