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  9312  cflecard  9675  sqrlem7  14608  setciso  17351  lsmss1  18791  sincosq1lem  25083  pjcompi  29449  mdsl1i  30098  dfon2lem3  33030  dfon2lem7  33034  tan2h  34899  dvasin  34993  ismrc  39318  nnsum4primes4  43974  nnsum4primesprm  43976  nnsum4primesgbe  43978  nnsum4primesle9  43980  rngciso  44273  rngcisoALTV  44285  ringciso  44324  ringcisoALTV  44348  aacllem  44922