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  9893  cflecard  10323  01sqrexlem7  15408  setciso  18259  lsmss1  19872  rngciso  20883  ringciso  20917  sincosq1lem  26819  pjcompi  32267  mdsl1i  32916  dfon2lem3  36527  dfon2lem7  36531  tan2h  38515  dvasin  38602  ismrc  43691  nnsum4primes4  48856  nnsum4primesprm  48858  nnsum4primesgbe  48860  nnsum4primesle9  48862  rngcisoALTV  49343  ringcisoALTV  49377  aacllem  50908