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  9591  dfom3  9617  dfac5lem4  10111  dfac9  10121  cflem  10229  cflemOLD  10230  canthp1lem2  10639  addsrpr  11061  mulsrpr  11062  trclublem  15034  gcdaddmlem  16583  tgjustf  28720  sto1i  32566  stji1i  32572  kur14lem9  35684  dfon2lem4  36254  dfttc3gw  37012  rtrclex  44323  comptiunov2i  44412