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  9785  cflecard  10153  01sqrexlem7  15159  setciso  18002  lsmss1  19581  rngciso  20557  ringciso  20591  sincosq1lem  26436  pjcompi  31656  mdsl1i  32305  dfon2lem3  35850  dfon2lem7  35854  tan2h  37675  dvasin  37767  ismrc  42821  nnsum4primes4  47916  nnsum4primesprm  47918  nnsum4primesgbe  47920  nnsum4primesle9  47922  rngcisoALTV  48404  ringcisoALTV  48438  aacllem  49929