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  6527  tfrlemibxssdm  6603  dom2lem  7064  php5  7165  nnfi  7180  xpfi  7245  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  9960  xnegid  10277  eluzfz2  10452  fzsuc  10491  fzsuc2  10502  fzp1disj  10503  fzneuz  10524  fzp1nel  10527  nn0p1elfzo  10610  exbtwnzlemex  10700  flhalf  10757  modqval  10781  frec2uzsucd  10858  frecuzrdgsuc  10871  uzsinds  10901  seq3p1  10922  seqp1cd  10927  expubnd  11053  iexpcyc  11101  binom2sub1  11111  hashennn  11240  lswwrd  11372  eqs1  11417  pfxid  11479  wrdind  11515  wrd2ind  11516  pfxccatpfx2  11530  swrdccat3blem  11532  shftfval  11607  shftcan1  11620  cjval  11631  reval  11635  imval  11636  cjmulrcl  11673  addcj  11677  absval  11788  resqrexlemdecn  11799  resqrexlemnmsq  11804  resqrexlemnm  11805  absneg  11837  abscj  11839  sqabsadd  11842  sqabssub  11843  ltabs  11875  dfabsmax  12005  negfi  12016  fsum3  12178  trirecip  12292  fprodseq  12374  efval  12452  ege2le3  12462  efcan  12467  sinval  12493  cosval  12494  efi4p  12508  resin4p  12509  recos4p  12510  sincossq  12539  eirraplem  12568  iddvds  12595  1dvds  12596  bezoutlemstep  12798  coprmgcdb  12890  1idssfct  12917  exprmfct  12941  pwbdvdslemn  12968  phival  13019  odzphi  13053  oddprmdvds  13161  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsi  13315  ballotfilemfrci  13328  setsn0fun  13446  gzsumfzval  13769  0subm  13849  grprcan  13900  isgrpid2  13903  grpinvid  13923  mulgval  13983  mulgnn0z  14010  0subg  14060  qus0  14096  ghmker  14131  imasabl  14229  mgpplusgg  14327  mgpbasg  14330  mgpscag  14332  mgptsetg  14333  mgpdsg  14335  rngen1zr0  14367  srgen1zr0  14398  opprmulfvalg  14483  opprsllem  14487  1unit  14522  1rinv  14543  subrngmcl  14625  subrg1  14647  subrgmcl  14649  subrgdvds  14651  subrguss  14652  subrginv  14653  subrgdv  14654  subrgunit  14655  subrgugrp  14656  rnrhmsubrg  14668  lmodfopne  14771  lsssn0  14815  lspsn0  14867  lsp0  14868  sralmod  14895  2idlval  14947  cnfldneg  15018  zrhval  15060  psrdifi  15211  psrdirfi  15212  cldval  15342  ntrfval  15343  clsfval  15344  neifval  15383  tx1cn  15512  ismet  15587  isxmet  15588  divcnap  15808  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  sgmnncl  16274  1lgs  16384  lgs1  16385  uhgredgiedgb  16597  uhgriedg0edg0  16598  subgrprop3  16725  wlklenvm1  16804  wlklenvm1g  16805  wlkl1loop  16821  wlklenvclwlk  16836  umgrclwwlkge2  16865  clwwlknp  16880  bj-charfun  17055  bj-findis  17227