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  7350  ordiso2  7375  omp1eomlem  7434  nnnninfeq2  7469  onenon  7529  oncardval  7531  cardonle  7532  recidnq  7760  archnqq  7784  prarloclemarch2  7786  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  recexprlemex  8004  0idsr  8134  lep1  9176  suprlubex  9283  uz11  9947  xnegid  10263  eluzfz2  10438  fzsuc  10477  fzsuc2  10488  fzp1disj  10489  fzneuz  10510  fzp1nel  10513  nn0p1elfzo  10596  exbtwnzlemex  10686  flhalf  10739  modqval  10763  frec2uzsucd  10840  frecuzrdgsuc  10853  uzsinds  10883  seq3p1  10904  seqp1cd  10909  expubnd  11035  iexpcyc  11083  binom2sub1  11093  hashennn  11221  lswwrd  11353  eqs1  11398  pfxid  11460  wrdind  11496  wrd2ind  11497  pfxccatpfx2  11511  swrdccat3blem  11513  shftfval  11588  shftcan1  11601  cjval  11612  reval  11616  imval  11617  cjmulrcl  11654  addcj  11658  absval  11769  resqrexlemdecn  11780  resqrexlemnmsq  11785  resqrexlemnm  11786  absneg  11818  abscj  11820  sqabsadd  11823  sqabssub  11824  ltabs  11855  dfabsmax  11985  negfi  11996  fsum3  12156  trirecip  12270  fprodseq  12352  efval  12430  ege2le3  12440  efcan  12445  sinval  12471  cosval  12472  efi4p  12486  resin4p  12487  recos4p  12488  sincossq  12517  eirraplem  12546  iddvds  12573  1dvds  12574  bezoutlemstep  12776  coprmgcdb  12868  1idssfct  12895  exprmfct  12918  oddpwdclemdc  12953  phival  12993  odzphi  13027  oddprmdvds  13135  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemsi  13260  ballotfilemfrci  13273  setsn0fun  13391  gzsumfzval  13713  0subm  13793  grprcan  13844  isgrpid2  13847  grpinvid  13867  mulgval  13927  mulgnn0z  13954  0subg  14004  qus0  14040  ghmker  14075  imasabl  14142  mgpplusgg  14223  mgpbasg  14226  mgpscag  14228  mgptsetg  14229  mgpdsg  14231  rngen1zr0  14263  srgen1zr0  14294  opprmulfvalg  14377  opprsllem  14381  1unit  14416  1rinv  14437  subrngmcl  14519  subrg1  14541  subrgmcl  14543  subrgdvds  14545  subrguss  14546  subrginv  14547  subrgdv  14548  subrgunit  14549  subrgugrp  14550  rnrhmsubrg  14562  lmodfopne  14665  lsssn0  14709  lspsn0  14761  lsp0  14762  sralmod  14789  2idlval  14841  cnfldneg  14912  zrhval  14954  psrbagfsupp  15057  cldval  15202  ntrfval  15203  clsfval  15204  neifval  15243  tx1cn  15372  ismet  15447  isxmet  15448  divcnap  15668  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  sgmnncl  16108  1lgs  16174  lgs1  16175  uhgredgiedgb  16387  uhgriedg0edg0  16388  subgrprop3  16515  wlklenvm1  16594  wlklenvm1g  16595  wlkl1loop  16611  wlklenvclwlk  16626  umgrclwwlkge2  16655  clwwlknp  16670  bj-charfun  16845  bj-findis  17017