Theorem mpan2i 696

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 693	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  tcwf  9296  cflecard  9664  sqrlem7  14600  setciso  17343  lsmss1  18783  sincosq1lem  25090  pjcompi  29455  mdsl1i  30104  dfon2lem3  33143  dfon2lem7  33147  tan2h  35049  dvasin  35141  ismrc  39642  nnsum4primes4  44307  nnsum4primesprm  44309  nnsum4primesgbe  44311  nnsum4primesle9  44313  rngciso  44606  rngcisoALTV  44618  ringciso  44657  ringcisoALTV  44681  aacllem  45329