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  15210  setciso  18058  lsmss1  19640  rngciso  20615  ringciso  20649  sincosq1lem  26461  pjcompi  31743  mdsl1i  32392  dfon2lem3  35965  dfon2lem7  35969  tan2h  37933  dvasin  38025  ismrc  43133  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum4primesgbe  48269  nnsum4primesle9  48271  rngcisoALTV  48753  ringcisoALTV  48787  aacllem  50276