Theorem mpan2i 707

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

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  tcwf  9834  cflecard  10202  01sqrexlem7  15265  setciso  18114  lsmss1  19695  rngciso  20674  ringciso  20708  sincosq1lem  26549  pjcompi  31831  mdsl1i  32480  dfon2lem3  36093  dfon2lem7  36097  tan2h  38071  dvasin  38163  ismrc  43242  nnsum4primes4  48371  nnsum4primesprm  48373  nnsum4primesgbe  48375  nnsum4primesle9  48377  rngcisoALTV  48859  ringcisoALTV  48893  aacllem  50382