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  9865  cflecard  10254  01sqrexlem7  15335  setciso  18180  lsmss1  19792  rngciso  20800  ringciso  20834  sincosq1lem  26735  pjcompi  32153  mdsl1i  32802  dfon2lem3  36362  dfon2lem7  36366  tan2h  38366  dvasin  38453  ismrc  43546  nnsum4primes4  48705  nnsum4primesprm  48707  nnsum4primesgbe  48709  nnsum4primesle9  48711  rngcisoALTV  49192  ringcisoALTV  49226  aacllem  50772