Theorem mpan2i 698

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 695	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  9807  cflecard  10175  01sqrexlem7  15183  setciso  18027  lsmss1  19606  rngciso  20583  ringciso  20617  sincosq1lem  26474  pjcompi  31759  mdsl1i  32408  dfon2lem3  35996  dfon2lem7  36000  tan2h  37860  dvasin  37952  ismrc  43055  nnsum4primes4  48146  nnsum4primesprm  48148  nnsum4primesgbe  48150  nnsum4primesle9  48152  rngcisoALTV  48634  ringcisoALTV  48668  aacllem  50157