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

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  427  mpan2  429  biadanid  622  mpjaodan  810  mpd3an3  1379  eueq2dc  2999  csbiegf  3191  difsnb  3856  reusv3i  4603  fimadmfo  5622  fvmpt3  5781  ffvelcdmd  5838  fnressn  5895  fliftel1  5994  f1oiso2  6027  riota5f  6059  1stvalg  6370  2ndvalg  6371  brtpos2  6516  tfrlemibxssdm  6592  dom2lem  7052  php5  7153  nnfi  7168  xpfi  7233  supisoti  7344  ordiso2  7369  omp1eomlem  7428  nnnninfeq2  7463  onenon  7523  oncardval  7525  cardonle  7526  recidnq  7754  archnqq  7778  prarloclemarch2  7780  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1l  7996  recexprlemss1u  7997  recexprlemex  7998  0idsr  8128  lep1  9169  suprlubex  9276  uz11  9928  xnegid  10244  eluzfz2  10419  fzsuc  10458  fzsuc2  10469  fzp1disj  10470  fzneuz  10491  fzp1nel  10494  nn0p1elfzo  10577  exbtwnzlemex  10667  flhalf  10720  modqval  10744  frec2uzsucd  10821  frecuzrdgsuc  10834  uzsinds  10864  seq3p1  10885  seqp1cd  10890  expubnd  11016  iexpcyc  11064  binom2sub1  11074  hashennn  11202  lswwrd  11334  eqs1  11379  pfxid  11441  wrdind  11477  wrd2ind  11478  pfxccatpfx2  11492  swrdccat3blem  11494  shftfval  11569  shftcan1  11582  cjval  11593  reval  11597  imval  11598  cjmulrcl  11635  addcj  11639  absval  11750  resqrexlemdecn  11761  resqrexlemnmsq  11766  resqrexlemnm  11767  absneg  11799  abscj  11801  sqabsadd  11804  sqabssub  11805  ltabs  11836  dfabsmax  11966  negfi  11977  fsum3  12137  trirecip  12251  fprodseq  12333  efval  12411  ege2le3  12421  efcan  12426  sinval  12452  cosval  12453  efi4p  12467  resin4p  12468  recos4p  12469  sincossq  12498  eirraplem  12527  iddvds  12554  1dvds  12555  bezoutlemstep  12757  coprmgcdb  12849  1idssfct  12876  exprmfct  12899  oddpwdclemdc  12934  phival  12974  odzphi  13008  oddprmdvds  13116  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemsi  13241  ballotfilemfrci  13254  setsn0fun  13372  gzsumfzval  13694  0subm  13774  grprcan  13825  isgrpid2  13828  grpinvid  13848  mulgval  13908  mulgnn0z  13935  0subg  13985  qus0  14021  ghmker  14056  imasabl  14123  mgpplusgg  14204  mgpbasg  14207  mgpscag  14209  mgptsetg  14210  mgpdsg  14212  rngen1zr0  14244  srgen1zr0  14275  opprmulfvalg  14358  opprsllem  14362  1unit  14397  1rinv  14418  subrngmcl  14500  subrg1  14522  subrgmcl  14524  subrgdvds  14526  subrguss  14527  subrginv  14528  subrgdv  14529  subrgunit  14530  subrgugrp  14531  rnrhmsubrg  14543  lmodfopne  14646  lsssn0  14690  lspsn0  14742  lsp0  14743  sralmod  14770  2idlval  14822  cnfldneg  14893  zrhval  14935  psrbagfsupp  15038  cldval  15183  ntrfval  15184  clsfval  15185  neifval  15224  tx1cn  15353  ismet  15428  isxmet  15429  divcnap  15649  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  sgmnncl  16085  1lgs  16145  lgs1  16146  uhgredgiedgb  16358  uhgriedg0edg0  16359  subgrprop3  16486  wlklenvm1  16565  wlklenvm1g  16566  wlkl1loop  16582  wlklenvclwlk  16597  umgrclwwlkge2  16626  clwwlknp  16641  bj-charfun  16816  bj-findis  16988