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  9843  cflecard  10213  01sqrexlem7  15221  setciso  18060  lsmss1  19602  rngciso  20554  ringciso  20588  sincosq1lem  26413  pjcompi  31608  mdsl1i  32257  dfon2lem3  35780  dfon2lem7  35784  tan2h  37613  dvasin  37705  ismrc  42696  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum4primesgbe  47798  nnsum4primesle9  47800  rngcisoALTV  48269  ringcisoALTV  48303  aacllem  49794