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  9345  cflecard  9713  sqrlem7  14656  setciso  17417  lsmss1  18858  sincosq1lem  25189  pjcompi  29554  mdsl1i  30203  dfon2lem3  33277  dfon2lem7  33281  tan2h  35351  dvasin  35443  ismrc  40037  nnsum4primes4  44696  nnsum4primesprm  44698  nnsum4primesgbe  44700  nnsum4primesle9  44702  rngciso  44995  rngcisoALTV  45007  ringciso  45046  ringcisoALTV  45070  aacllem  45742