Theorem mp2ani 711

Description: An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mp2ani.1	⊢ 𝜓
mp2ani.2	⊢ 𝜒
mp2ani.3	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mp2ani	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2ani

Step	Hyp	Ref	Expression
1		mp2ani.2	. 2 ⊢ 𝜒
2		mp2ani.1	. . 3 ⊢ 𝜓
3		mp2ani.3	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpani 709	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpi 21	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  inf0  9625  dfom3  9651  dfac5lem4  10208  dfac9  10218  cflem  10326  canthp1lem2  10741  addsrpr  11163  mulsrpr  11164  trclublem  15153  gcdaddmlem  16701  tgjustf  28940  sto1i  32843  stji1i  32849  kur14lem9  36065  dfon2lem4  36640  dfttc3gw  37403  rtrclex  44710  comptiunov2i  44799