Theorem mpan2i 697

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  tcwf  9923  cflecard  10293  01sqrexlem7  15287  setciso  18136  lsmss1  19683  rngciso  20638  ringciso  20672  sincosq1lem  26539  pjcompi  31691  mdsl1i  32340  dfon2lem3  35786  dfon2lem7  35790  tan2h  37619  dvasin  37711  ismrc  42712  nnsum4primes4  47776  nnsum4primesprm  47778  nnsum4primesgbe  47780  nnsum4primesle9  47782  rngcisoALTV  48193  ringcisoALTV  48227  aacllem  49320