Theorem mpan2i 694

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 691	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 206  df-an 396

This theorem is referenced by:  tcwf  9884  cflecard  10254  01sqrexlem7  15202  setciso  18051  lsmss1  19581  rngciso  20530  ringciso  20564  sincosq1lem  26347  pjcompi  31358  mdsl1i  32007  dfon2lem3  35227  dfon2lem7  35231  tan2h  36944  dvasin  37036  ismrc  41902  nnsum4primes4  46916  nnsum4primesprm  46918  nnsum4primesgbe  46920  nnsum4primesle9  46922  rngcisoALTV  47114  ringcisoALTV  47148  aacllem  48010