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  9795  cflecard  10163  01sqrexlem7  15171  setciso  18015  lsmss1  19594  rngciso  20571  ringciso  20605  sincosq1lem  26462  pjcompi  31747  mdsl1i  32396  dfon2lem3  35977  dfon2lem7  35981  tan2h  37813  dvasin  37905  ismrc  42943  nnsum4primes4  48035  nnsum4primesprm  48037  nnsum4primesgbe  48039  nnsum4primesle9  48041  rngcisoALTV  48523  ringcisoALTV  48557  aacllem  50046