Theorem mpan2i 698

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 695	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  9798  cflecard  10166  01sqrexlem7  15201  setciso  18049  lsmss1  19631  rngciso  20606  ringciso  20640  sincosq1lem  26474  pjcompi  31758  mdsl1i  32407  dfon2lem3  35981  dfon2lem7  35985  tan2h  37947  dvasin  38039  ismrc  43147  nnsum4primes4  48277  nnsum4primesprm  48279  nnsum4primesgbe  48281  nnsum4primesle9  48283  rngcisoALTV  48765  ringcisoALTV  48799  aacllem  50288