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  9836  cflecard  10206  01sqrexlem7  15214  setciso  18053  lsmss1  19595  rngciso  20547  ringciso  20581  sincosq1lem  26406  pjcompi  31601  mdsl1i  32250  dfon2lem3  35773  dfon2lem7  35777  tan2h  37606  dvasin  37698  ismrc  42689  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum4primesle9  47796  rngcisoALTV  48265  ringcisoALTV  48299  aacllem  49790