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 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  9906  cflecard  10276  01sqrexlem7  15227  setciso  18079  lsmss1  19619  rngciso  20570  ringciso  20604  sincosq1lem  26431  pjcompi  31481  mdsl1i  32130  dfon2lem3  35381  dfon2lem7  35385  tan2h  37085  dvasin  37177  ismrc  42121  nnsum4primes4  47129  nnsum4primesprm  47131  nnsum4primesgbe  47133  nnsum4primesle9  47135  rngcisoALTV  47339  ringcisoALTV  47373  aacllem  48234