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 207  df-an 396

This theorem is referenced by:  tcwf  9952  cflecard  10322  01sqrexlem7  15297  setciso  18158  lsmss1  19707  rngciso  20660  ringciso  20694  sincosq1lem  26557  pjcompi  31704  mdsl1i  32353  dfon2lem3  35749  dfon2lem7  35753  tan2h  37572  dvasin  37664  ismrc  42657  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum4primesle9  47669  rngcisoALTV  48000  ringcisoALTV  48034  aacllem  48895