Theorem mpan2i 693

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 690	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 206  df-an 396

This theorem is referenced by:  tcwf  9572  cflecard  9940  sqrlem7  14888  setciso  17722  lsmss1  19186  sincosq1lem  25559  pjcompi  29935  mdsl1i  30584  dfon2lem3  33667  dfon2lem7  33671  tan2h  35696  dvasin  35788  ismrc  40439  nnsum4primes4  45129  nnsum4primesprm  45131  nnsum4primesgbe  45133  nnsum4primesle9  45135  rngciso  45428  rngcisoALTV  45440  ringciso  45479  ringcisoALTV  45503  aacllem  46391