Theorem mpdan 649

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 642	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mpan2  652  mpjaodan  761  mpd3an3  1278  eueq2  3010  csbiegf  3176  difsnb  3850  ltfinp1  4462  vfinncsp  4554  addccan2  4559  fnressn  5438  f1oiso2  5500  fvdomfn  5868  fvranfn  5869  qsdisj  5995  enadj  6060  enmap2lem3  6065  enmap1lem3  6071  nclecid  6197  le0nc  6200  nnltp1c  6262  nmembers1  6271