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  3011  csbiegf  3177  difsnb  3851  ltfinp1  4463  vfinncsp  4555  addccan2  4560  fnressn  5439  f1oiso2  5501  fvdomfn  5869  fvranfn  5870  qsdisj  5996  enadj  6061  enmap2lem3  6066  enmap1lem3  6072  nclecid  6198  le0nc  6201  nnltp1c  6263  nmembers1  6272