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  616  mpjaodan  803  mpd3an3  1372  eueq2dc  2976  csbiegf  3168  difsnb  3811  reusv3i  4550  fimadmfo  5559  fvmpt3  5715  ffvelcdmd  5773  fnressn  5829  fliftel1  5924  f1oiso2  5957  riota5f  5987  1stvalg  6294  2ndvalg  6295  brtpos2  6403  tfrlemibxssdm  6479  dom2lem  6931  php5  7027  nnfi  7042  xpfi  7102  supisoti  7185  ordiso2  7210  omp1eomlem  7269  nnnninfeq2  7304  onenon  7364  oncardval  7366  cardonle  7367  recidnq  7588  archnqq  7612  prarloclemarch2  7614  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1l  7830  recexprlemss1u  7831  recexprlemex  7832  0idsr  7962  lep1  9000  suprlubex  9107  uz11  9753  xnegid  10063  eluzfz2  10236  fzsuc  10273  fzsuc2  10283  fzp1disj  10284  fzneuz  10305  fzp1nel  10308  exbtwnzlemex  10477  flhalf  10530  modqval  10554  frec2uzsucd  10631  frecuzrdgsuc  10644  uzsinds  10674  seq3p1  10695  seqp1cd  10700  expubnd  10826  iexpcyc  10874  binom2sub1  10884  hashennn  11010  lswwrd  11126  eqs1  11169  pfxid  11226  wrdind  11262  wrd2ind  11263  pfxccatpfx2  11277  swrdccat3blem  11279  shftfval  11340  shftcan1  11353  cjval  11364  reval  11368  imval  11369  cjmulrcl  11406  addcj  11410  absval  11520  resqrexlemdecn  11531  resqrexlemnmsq  11536  resqrexlemnm  11537  absneg  11569  abscj  11571  sqabsadd  11574  sqabssub  11575  ltabs  11606  dfabsmax  11736  negfi  11747  fsum3  11906  trirecip  12020  fprodseq  12102  efval  12180  ege2le3  12190  efcan  12195  sinval  12221  cosval  12222  efi4p  12236  resin4p  12237  recos4p  12238  sincossq  12267  eirraplem  12296  iddvds  12323  1dvds  12324  bezoutlemstep  12526  coprmgcdb  12618  1idssfct  12645  exprmfct  12668  oddpwdclemdc  12703  phival  12743  odzphi  12777  oddprmdvds  12885  setsn0fun  13077  gsumfzval  13432  0subm  13525  gsumfzz  13536  grprcan  13578  isgrpid2  13581  grpinvid  13601  mulgval  13667  mulgnn0z  13694  0subg  13744  qus0  13780  ghmker  13815  imasabl  13881  mgpplusgg  13895  mgpbasg  13897  mgpscag  13898  mgptsetg  13899  mgpdsg  13901  srgen1zr  13959  opprmulfvalg  14041  opprsllem  14045  1unit  14079  1rinv  14100  subrngmcl  14181  subrg1  14203  subrgmcl  14205  subrgdvds  14207  subrguss  14208  subrginv  14209  subrgdv  14210  subrgunit  14211  subrgugrp  14212  rnrhmsubrg  14224  lmodfopne  14298  lsssn0  14342  lspsn0  14394  lsp0  14395  sralmod  14422  2idlval  14474  cnfldneg  14545  zrhval  14589  cldval  14781  ntrfval  14782  clsfval  14783  neifval  14822  tx1cn  14951  ismet  15026  isxmet  15027  divcnap  15247  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  sgmnncl  15670  1lgs  15730  lgs1  15731  uhgredgiedgb  15940  uhgriedg0edg0  15941  wlklenvm1  16062  wlklenvm1g  16063  wlkl1loop  16079  wlklenvclwlk  16094  bj-charfun  16194  bj-findis  16366