Theorem mpan2i 709

Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2i.1	⊢ 𝜒
mpan2i.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpan2i	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpan2i

Step	Hyp	Ref	Expression
1		mpan2i.1	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		mpan2i.2	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpan2d 706	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  tcwf  9843  cflecard  10224  01sqrexlem7  15287  setciso  18136  lsmss1  19723  rngciso  20711  ringciso  20745  sincosq1lem  26616  pjcompi  31929  mdsl1i  32578  dfon2lem3  36141  dfon2lem7  36145  tan2h  38118  dvasin  38210  ismrc  43289  nnsum4primes4  48410  nnsum4primesprm  48412  nnsum4primesgbe  48414  nnsum4primesle9  48416  rngcisoALTV  48898  ringcisoALTV  48932  aacllem  50431