Theorem mpdan 398

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

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  mpan2  401  mpjaodan  711  mpd3an3  1233  eueq2dc  2714  csbiegf  2890  difsnb  3506  reusv3i  4191  fvmpt3  5251  ffvelrnd  5303  fnressn  5349  fliftel1  5434  f1oiso2  5466  riota5f  5492  1stvalg  5769  2ndvalg  5770  brtpos2  5866  tfrlemibxssdm  5941  dom2lem  6252  php5  6321  nnfi  6333  ordiso2  6357  onenon  6364  oncardval  6366  cardonle  6367  recidnq  6491  archnqq  6515  prarloclemarch2  6517  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  recexprlemex  6735  0idsr  6852  lep1  7811  uz11  8495  eluzfz2  8896  fzsuc  8931  fzsuc2  8941  fzp1disj  8942  fzneuz  8963  fzp1nel  8966  flhalf  9144  modqval  9166  frecuzrdgsuc  9201  iseqcl  9223  iseqp1  9225  expubnd  9311  shftfval  9422  shftcan1  9435  cjval  9445  reval  9449  imval  9450  cjmulrcl  9487  addcj  9491  absval  9599  resqrexlemdecn  9610  resqrexlemnmsq  9615  resqrexlemnm  9616  absneg  9648  abscj  9650  sqabsadd  9653  sqabssub  9654  ltabs  9683  bj-findis  10104