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  9540  dfom3  9566  dfac5lem4  10046  dfac5lem4OLD  10048  dfac9  10057  cflem  10165  cflemOLD  10166  canthp1lem2  10574  addsrpr  10996  mulsrpr  10997  trclublem  14955  gcdaddmlem  16491  tgjustf  28566  sto1i  32332  stji1i  32338  kur14lem9  35449  dfon2lem4  36019  dfttc3gw  36758  rtrclex  44068  comptiunov2i  44157