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  9937  cflecard  10369  01sqrexlem7  15458  setciso  18316  lsmss1  19930  rngciso  20941  ringciso  20975  sincosq1lem  26883  pjcompi  32331  mdsl1i  32980  dfon2lem3  36762  dfon2lem7  36766  tan2h  38803  dvasin  38890  ismrc  43978  nnsum4primes4  49160  nnsum4primesprm  49162  nnsum4primesgbe  49164  nnsum4primesle9  49166  rngcisoALTV  49647  ringcisoALTV  49681  aacllem  51367