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  9776  cflecard  10144  01sqrexlem7  15155  setciso  17998  lsmss1  19578  rngciso  20554  ringciso  20588  sincosq1lem  26434  pjcompi  31650  mdsl1i  32299  dfon2lem3  35825  dfon2lem7  35829  tan2h  37658  dvasin  37750  ismrc  42740  nnsum4primes4  47826  nnsum4primesprm  47828  nnsum4primesgbe  47830  nnsum4primesle9  47832  rngcisoALTV  48314  ringcisoALTV  48348  aacllem  49839