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  9921  cflecard  10291  01sqrexlem7  15284  setciso  18145  lsmss1  19698  rngciso  20655  ringciso  20689  sincosq1lem  26554  pjcompi  31701  mdsl1i  32350  dfon2lem3  35767  dfon2lem7  35771  tan2h  37599  dvasin  37691  ismrc  42689  nnsum4primes4  47714  nnsum4primesprm  47716  nnsum4primesgbe  47718  nnsum4primesle9  47720  rngcisoALTV  48121  ringcisoALTV  48155  aacllem  49032