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 396

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 397

This theorem is referenced by:  tcwf  9641  cflecard  10009  sqrlem7  14960  setciso  17806  lsmss1  19271  sincosq1lem  25654  pjcompi  30034  mdsl1i  30683  dfon2lem3  33761  dfon2lem7  33765  tan2h  35769  dvasin  35861  ismrc  40523  nnsum4primes4  45241  nnsum4primesprm  45243  nnsum4primesgbe  45245  nnsum4primesle9  45247  rngciso  45540  rngcisoALTV  45552  ringciso  45591  ringcisoALTV  45615  aacllem  46505