Theorem mpdan 418

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpidan  420  mpan2  422  mpjaodan  788  mpd3an3  1327  eueq2dc  2894  csbiegf  3083  difsnb  3710  reusv3i  4431  fvmpt3  5559  ffvelrnd  5615  fnressn  5665  fliftel1  5756  f1oiso2  5789  riota5f  5816  1stvalg  6102  2ndvalg  6103  brtpos2  6210  tfrlemibxssdm  6286  dom2lem  6729  php5  6815  nnfi  6829  xpfi  6886  supisoti  6966  ordiso2  6991  omp1eomlem  7050  nnnninfeq2  7084  onenon  7131  oncardval  7133  cardonle  7134  recidnq  7325  archnqq  7349  prarloclemarch2  7351  recexprlem1ssl  7565  recexprlem1ssu  7566  recexprlemss1l  7567  recexprlemss1u  7568  recexprlemex  7569  0idsr  7699  lep1  8731  suprlubex  8838  uz11  9479  xnegid  9786  eluzfz2  9957  fzsuc  9994  fzsuc2  10004  fzp1disj  10005  fzneuz  10026  fzp1nel  10029  exbtwnzlemex  10175  flhalf  10227  modqval  10249  frec2uzsucd  10326  frecuzrdgsuc  10339  uzsinds  10367  seq3p1  10387  seqp1cd  10391  expubnd  10502  iexpcyc  10549  binom2sub1  10558  hashennn  10682  shftfval  10749  shftcan1  10762  cjval  10773  reval  10777  imval  10778  cjmulrcl  10815  addcj  10819  absval  10929  resqrexlemdecn  10940  resqrexlemnmsq  10945  resqrexlemnm  10946  absneg  10978  abscj  10980  sqabsadd  10983  sqabssub  10984  ltabs  11015  dfabsmax  11145  negfi  11155  fsum3  11314  trirecip  11428  fprodseq  11510  efval  11588  ege2le3  11598  efcan  11603  sinval  11629  cosval  11630  efi4p  11644  resin4p  11645  recos4p  11646  sincossq  11675  eirraplem  11703  iddvds  11730  1dvds  11731  bezoutlemstep  11915  coprmgcdb  11999  1idssfct  12026  exprmfct  12049  oddpwdclemdc  12082  phival  12122  odzphi  12155  oddprmdvds  12261  setsn0fun  12368  cldval  12640  ntrfval  12641  clsfval  12642  neifval  12681  tx1cn  12810  ismet  12885  isxmet  12886  divcnap  13096  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  bj-charfun  13524  bj-findis  13696