Theorem mpan2i 695

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 692	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  9306  cflecard  9669  sqrlem7  14602  setciso  17345  lsmss1  18785  sincosq1lem  25077  pjcompi  29443  mdsl1i  30092  dfon2lem3  33025  dfon2lem7  33029  tan2h  34878  dvasin  34972  ismrc  39291  nnsum4primes4  43948  nnsum4primesprm  43950  nnsum4primesgbe  43952  nnsum4primesle9  43954  rngciso  44247  rngcisoALTV  44259  ringciso  44298  ringcisoALTV  44322  aacllem  44896