Theorem mp2ani 704

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  inf0  9533  dfom3  9559  dfac5lem4  10039  dfac5lem4OLD  10041  dfac9  10050  cflem  10158  cflemOLD  10159  canthp1lem2  10567  addsrpr  10989  mulsrpr  10990  trclublem  14948  gcdaddmlem  16484  tgjustf  28559  sto1i  32325  stji1i  32331  kur14lem9  35442  dfon2lem4  36012  dfttc3gw  36751  rtrclex  44061  comptiunov2i  44150