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  9902  cflecard  10272  01sqrexlem7  15272  setciso  18109  lsmss1  19651  rngciso  20603  ringciso  20637  sincosq1lem  26463  pjcompi  31658  mdsl1i  32307  dfon2lem3  35808  dfon2lem7  35812  tan2h  37641  dvasin  37733  ismrc  42691  nnsum4primes4  47770  nnsum4primesprm  47772  nnsum4primesgbe  47774  nnsum4primesle9  47776  rngcisoALTV  48219  ringcisoALTV  48253  aacllem  49632