Theorem mp2ani 697

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 695	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpi 20	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  inf0  9616  dfom3  9642  dfac5lem4  10121  dfac9  10131  cflem  10241  canthp1lem2  10648  addsrpr  11070  mulsrpr  11071  trclublem  14942  gcdaddmlem  16465  tgjustf  27724  sto1i  31489  stji1i  31495  kur14lem9  34205  dfon2lem4  34758  rtrclex  42368  comptiunov2i  42457