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  9858  cflecard  10247  01sqrexlem7  15318  setciso  18165  lsmss1  19758  rngciso  20766  ringciso  20800  sincosq1lem  26691  pjcompi  32053  mdsl1i  32702  dfon2lem3  36288  dfon2lem7  36292  tan2h  38296  dvasin  38388  ismrc  43465  nnsum4primes4  48587  nnsum4primesprm  48589  nnsum4primesgbe  48591  nnsum4primesle9  48593  rngcisoALTV  49075  ringcisoALTV  49109  aacllem  50654