Theorem mpdan 421

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 411	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpidan  423  mpan2  425  biadanid  618  mpjaodan  806  mpd3an3  1375  eueq2dc  2992  csbiegf  3184  difsnb  3839  reusv3i  4582  fimadmfo  5601  fvmpt3  5758  ffvelcdmd  5815  fnressn  5872  fliftel1  5969  f1oiso2  6002  riota5f  6032  1stvalg  6338  2ndvalg  6339  brtpos2  6484  tfrlemibxssdm  6560  dom2lem  7013  php5  7114  nnfi  7129  xpfi  7194  supisoti  7303  ordiso2  7328  omp1eomlem  7387  nnnninfeq2  7422  onenon  7482  oncardval  7484  cardonle  7485  recidnq  7713  archnqq  7737  prarloclemarch2  7739  recexprlem1ssl  7953  recexprlem1ssu  7954  recexprlemss1l  7955  recexprlemss1u  7956  recexprlemex  7957  0idsr  8087  lep1  9124  suprlubex  9231  uz11  9883  xnegid  10198  eluzfz2  10372  fzsuc  10409  fzsuc2  10420  fzp1disj  10421  fzneuz  10442  fzp1nel  10445  nn0p1elfzo  10528  exbtwnzlemex  10616  flhalf  10669  modqval  10693  frec2uzsucd  10770  frecuzrdgsuc  10783  uzsinds  10813  seq3p1  10834  seqp1cd  10839  expubnd  10965  iexpcyc  11013  binom2sub1  11023  hashennn  11151  lswwrd  11279  eqs1  11324  pfxid  11386  wrdind  11422  wrd2ind  11423  pfxccatpfx2  11437  swrdccat3blem  11439  shftfval  11514  shftcan1  11527  cjval  11538  reval  11542  imval  11543  cjmulrcl  11580  addcj  11584  absval  11694  resqrexlemdecn  11705  resqrexlemnmsq  11710  resqrexlemnm  11711  absneg  11743  abscj  11745  sqabsadd  11748  sqabssub  11749  ltabs  11780  dfabsmax  11910  negfi  11921  fsum3  12081  trirecip  12195  fprodseq  12277  efval  12355  ege2le3  12365  efcan  12370  sinval  12396  cosval  12397  efi4p  12411  resin4p  12412  recos4p  12413  sincossq  12442  eirraplem  12471  iddvds  12498  1dvds  12499  bezoutlemstep  12701  coprmgcdb  12793  1idssfct  12820  exprmfct  12843  oddpwdclemdc  12878  phival  12918  odzphi  12952  oddprmdvds  13060  ballotfilemfc0  13157  ballotfilemfcc  13158  setsn0fun  13270  gsumfzval  13625  0subm  13718  gsumfzz  13729  grprcan  13771  isgrpid2  13774  grpinvid  13794  mulgval  13860  mulgnn0z  13887  0subg  13937  qus0  13973  ghmker  14008  imasabl  14074  mgpplusgg  14089  mgpbasg  14091  mgpscag  14092  mgptsetg  14093  mgpdsg  14095  srgen1zr  14153  opprmulfvalg  14235  opprsllem  14239  1unit  14274  1rinv  14295  subrngmcl  14377  subrg1  14399  subrgmcl  14401  subrgdvds  14403  subrguss  14404  subrginv  14405  subrgdv  14406  subrgunit  14407  subrgugrp  14408  rnrhmsubrg  14420  ringen1zr  14483  lmodfopne  14523  lsssn0  14567  lspsn0  14619  lsp0  14620  sralmod  14647  2idlval  14699  cnfldneg  14770  zrhval  14814  psrbagfsupp  14868  cldval  15013  ntrfval  15014  clsfval  15015  neifval  15054  tx1cn  15183  ismet  15258  isxmet  15259  divcnap  15479  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  sgmnncl  15905  1lgs  15965  lgs1  15966  uhgredgiedgb  16178  uhgriedg0edg0  16179  subgrprop3  16306  wlklenvm1  16385  wlklenvm1g  16386  wlkl1loop  16402  wlklenvclwlk  16417  umgrclwwlkge2  16446  clwwlknp  16461  bj-charfun  16626  bj-findis  16798