Theorem mpan2i 710

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 707	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tcwf  9904  cflecard  10334  01sqrexlem7  15421  setciso  18272  lsmss1  19885  rngciso  20896  ringciso  20930  sincosq1lem  26832  pjcompi  32280  mdsl1i  32929  dfon2lem3  36640  dfon2lem7  36644  tan2h  38629  dvasin  38716  ismrc  43806  nnsum4primes4  48981  nnsum4primesprm  48983  nnsum4primesgbe  48985  nnsum4primesle9  48987  rngcisoALTV  49468  ringcisoALTV  49502  aacllem  51108