Theorem mpan2i 703

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 700	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  tcwf  9805  cflecard  10173  01sqrexlem7  15208  setciso  18056  lsmss1  19638  rngciso  20617  ringciso  20651  sincosq1lem  26486  pjcompi  31768  mdsl1i  32417  dfon2lem3  36018  dfon2lem7  36022  tan2h  37986  dvasin  38078  ismrc  43157  nnsum4primes4  48287  nnsum4primesprm  48289  nnsum4primesgbe  48291  nnsum4primesle9  48293  rngcisoALTV  48775  ringcisoALTV  48809  aacllem  50298