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  7062  php5  7163  nnfi  7178  xpfi  7243  supisoti  7356  ordiso2  7381  omp1eomlem  7440  nnnninfeq2  7475  onenon  7535  oncardval  7537  cardonle  7538  recidnq  7766  archnqq  7790  prarloclemarch2  7792  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  recexprlemex  8010  0idsr  8140  lep1  9183  suprlubex  9290  uz11  9961  xnegid  10278  eluzfz2  10453  fzsuc  10492  fzsuc2  10503  fzp1disj  10504  fzneuz  10525  fzp1nel  10528  nn0p1elfzo  10611  exbtwnzlemex  10701  flhalf  10758  modqval  10782  frec2uzsucd  10859  frecuzrdgsuc  10872  uzsinds  10902  seq3p1  10923  seqp1cd  10928  expubnd  11054  iexpcyc  11102  binom2sub1  11112  hashennn  11241  lswwrd  11373  eqs1  11418  pfxid  11480  wrdind  11516  wrd2ind  11517  pfxccatpfx2  11531  swrdccat3blem  11533  shftfval  11608  shftcan1  11621  cjval  11632  reval  11636  imval  11637  cjmulrcl  11674  addcj  11678  absval  11789  resqrexlemdecn  11800  resqrexlemnmsq  11805  resqrexlemnm  11806  absneg  11838  abscj  11840  sqabsadd  11843  sqabssub  11844  ltabs  11876  dfabsmax  12006  negfi  12017  fsum3  12179  trirecip  12293  fprodseq  12375  efval  12453  ege2le3  12463  efcan  12468  sinval  12494  cosval  12495  efi4p  12509  resin4p  12510  recos4p  12511  sincossq  12540  eirraplem  12569  iddvds  12596  1dvds  12597  bezoutlemstep  12799  coprmgcdb  12891  1idssfct  12918  exprmfct  12942  pwbdvdslemn  12969  phival  13020  odzphi  13054  oddprmdvds  13162  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsi  13316  ballotfilemfrci  13329  setsn0fun  13447  gzsumfzval  13770  0subm  13850  grprcan  13901  isgrpid2  13904  grpinvid  13924  mulgval  13984  mulgnn0z  14011  0subg  14061  qus0  14097  ghmker  14132  imasabl  14230  mgpplusgg  14328  mgpbasg  14331  mgpscag  14333  mgptsetg  14334  mgpdsg  14336  rngen1zr0  14368  srgen1zr0  14399  opprmulfvalg  14484  opprsllem  14488  1unit  14523  1rinv  14544  subrngmcl  14626  subrg1  14648  subrgmcl  14650  subrgdvds  14652  subrguss  14653  subrginv  14654  subrgdv  14655  subrgunit  14656  subrgugrp  14657  rnrhmsubrg  14669  lmodfopne  14772  lsssn0  14816  lspsn0  14868  lsp0  14869  sralmod  14896  2idlval  14948  cnfldneg  15019  zrhval  15061  psrbagfsupp  15164  cldval  15322  ntrfval  15323  clsfval  15324  neifval  15363  tx1cn  15492  ismet  15567  isxmet  15568  divcnap  15788  dvaddxxbr  15924  dvmulxxbr  15925  dvcoapbr  15930  sgmnncl  16254  1lgs  16364  lgs1  16365  uhgredgiedgb  16577  uhgriedg0edg0  16578  subgrprop3  16705  wlklenvm1  16784  wlklenvm1g  16785  wlkl1loop  16801  wlklenvclwlk  16816  umgrclwwlkge2  16845  clwwlknp  16860  bj-charfun  17035  bj-findis  17207