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  9798  cflecard  10166  01sqrexlem7  15173  setciso  18016  lsmss1  19562  rngciso  20541  ringciso  20575  sincosq1lem  26422  pjcompi  31634  mdsl1i  32283  dfon2lem3  35761  dfon2lem7  35765  tan2h  37594  dvasin  37686  ismrc  42677  nnsum4primes4  47777  nnsum4primesprm  47779  nnsum4primesgbe  47781  nnsum4primesle9  47783  rngcisoALTV  48265  ringcisoALTV  48299  aacllem  49790