Theorem mp2ani 710

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  inf0  9578  dfom3  9604  dfac5lem4  10098  dfac9  10108  cflem  10216  cflemOLD  10217  canthp1lem2  10626  addsrpr  11048  mulsrpr  11049  trclublem  15022  gcdaddmlem  16572  tgjustf  28700  sto1i  32497  stji1i  32503  kur14lem9  35577  dfon2lem4  36147  dfttc3gw  36896  rtrclex  44205  comptiunov2i  44294