Theorem mp2ani 708

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  inf0  9573  dfom3  9599  dfac5lem4  10079  dfac5lem4OLD  10081  dfac9  10090  cflem  10198  cflemOLD  10199  canthp1lem2  10608  addsrpr  11030  mulsrpr  11031  trclublem  15005  gcdaddmlem  16541  tgjustf  28619  sto1i  32385  stji1i  32391  kur14lem9  35528  dfon2lem4  36098  dfttc3gw  36847  rtrclex  44157  comptiunov2i  44246