Theorem mpdan 527

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpdan.1	⊢ (φ → ψ)
mpdan.2	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
mpdan	⊢ (φ → χ)

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		mpdan.1	. 2 ⊢ (φ → ψ)
2		mpdan.2	. . 3 ⊢ ((φ ∧ ψ) → χ)
3	2	exp 291	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mpd 46	1 ⊢ (φ → χ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  mpancom 528  eueq2 1429  eueq3 1430  supsn 2168  onsucuni 2335  fnressn 2897  oesuc 3134  oaordi 3148  dom2d 3307  canth2g 3382  php4 3412  onfin 3415  inf5 3472  trcl 3489  oncardval 3626  cardonle 3629  canth3 3656  cardaleph 3690  cfval 3701  cdavalt 3716  reclem3pr 3952  reclem4pr 3953  0idsr 4000  dividt 4256  zbtwnre 4619  ococint 5298  spanvalt 5300  pjocin 5583  pjclem4 5653  pj3s 5659

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org