Theorem mp2ani 699

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 697	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpi 20	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:  inf0  9542  dfom3  9568  dfac5lem4  10048  dfac5lem4OLD  10050  dfac9  10059  cflem  10167  cflemOLD  10168  canthp1lem2  10576  addsrpr  10998  mulsrpr  10999  trclublem  14957  gcdaddmlem  16493  tgjustf  28541  sto1i  32307  stji1i  32313  kur14lem9  35396  dfon2lem4  35966  dfttc3gw  36705  rtrclex  44044  comptiunov2i  44133