Theorem mpan2i 705

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  tcwf  9831  cflecard  10199  01sqrexlem7  15251  setciso  18100  lsmss1  19681  rngciso  20660  ringciso  20694  sincosq1lem  26532  pjcompi  31814  mdsl1i  32463  dfon2lem3  36081  dfon2lem7  36085  tan2h  38059  dvasin  38151  ismrc  43230  nnsum4primes4  48359  nnsum4primesprm  48361  nnsum4primesgbe  48363  nnsum4primesle9  48365  rngcisoALTV  48847  ringcisoALTV  48881  aacllem  50370