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  9767  cflecard  10135  01sqrexlem7  15142  setciso  17985  lsmss1  19531  rngciso  20507  ringciso  20541  sincosq1lem  26387  pjcompi  31603  mdsl1i  32252  dfon2lem3  35776  dfon2lem7  35780  tan2h  37609  dvasin  37701  ismrc  42691  nnsum4primes4  47787  nnsum4primesprm  47789  nnsum4primesgbe  47791  nnsum4primesle9  47793  rngcisoALTV  48275  ringcisoALTV  48309  aacllem  49800