Theorem mpan2i 680

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  tcwf  8993  cflecard  9360  sqrlem7  14212  setciso  16945  lsmss1  18280  sincosq1lem  24464  pjcompi  28859  mdsl1i  29508  dfon2lem3  32010  dfon2lem7  32014  tan2h  33714  dvasin  33808  ismrc  37766  nnsum4primes4  42252  nnsum4primesprm  42254  nnsum4primesgbe  42256  nnsum4primesle9  42258  rngciso  42550  rngcisoALTV  42562  ringciso  42601  ringcisoALTV  42625  aacllem  43118