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  9856  cflecard  10237  01sqrexlem7  15301  setciso  18149  lsmss1  19736  rngciso  20724  ringciso  20758  sincosq1lem  26643  pjcompi  32005  mdsl1i  32654  dfon2lem3  36256  dfon2lem7  36260  tan2h  38244  dvasin  38336  ismrc  43415  nnsum4primes4  48537  nnsum4primesprm  48539  nnsum4primesgbe  48541  nnsum4primesle9  48543  rngcisoALTV  49025  ringcisoALTV  49059  aacllem  50584