Theorem mpdan 412

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpidan  414  mpan2  416  mpjaodan  747  mpd3an3  1274  eueq2dc  2786  csbiegf  2969  difsnb  3575  reusv3i  4272  fvmpt3  5367  ffvelrnd  5419  fnressn  5467  fliftel1  5555  f1oiso2  5588  riota5f  5614  1stvalg  5895  2ndvalg  5896  brtpos2  5998  tfrlemibxssdm  6074  dom2lem  6469  php5  6554  nnfi  6568  xpfi  6619  supisoti  6684  ordiso2  6707  onenon  6791  oncardval  6793  cardonle  6794  recidnq  6931  archnqq  6955  prarloclemarch2  6957  recexprlem1ssl  7171  recexprlem1ssu  7172  recexprlemss1l  7173  recexprlemss1u  7174  recexprlemex  7175  0idsr  7292  lep1  8278  suprlubex  8385  uz11  9010  eluzfz2  9415  fzsuc  9450  fzsuc2  9460  fzp1disj  9461  fzneuz  9482  fzp1nel  9485  exbtwnzlemex  9626  flhalf  9674  modqval  9696  frec2uzsucd  9773  frecuzrdgsuc  9786  uzsinds  9813  iseqp1  9847  iseqp1t  9848  seq3p1  9849  expubnd  9977  iexpcyc  10024  binom2sub1  10033  hashennn  10153  shftfval  10220  shftcan1  10233  cjval  10244  reval  10248  imval  10249  cjmulrcl  10286  addcj  10290  absval  10399  resqrexlemdecn  10410  resqrexlemnmsq  10415  resqrexlemnm  10416  absneg  10448  abscj  10450  sqabsadd  10453  sqabssub  10454  ltabs  10485  dfabsmax  10615  negfi  10623  fisum  10742  trirecip  10856  iddvds  10902  1dvds  10903  bezoutlemstep  11079  coprmgcdb  11163  1idssfct  11190  exprmfct  11212  oddpwdclemdc  11244  phival  11282  bj-findis  11531