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  9604  dfom3  9630  dfac5lem4  10133  dfac9  10143  cflem  10251  canthp1lem2  10666  addsrpr  11088  mulsrpr  11089  trclublem  15072  gcdaddmlem  16620  tgjustf  28822  sto1i  32725  stji1i  32731  kur14lem9  35801  dfon2lem4  36371  dfttc3gw  37150  rtrclex  44465  comptiunov2i  44554