Theorem mp2ani 711

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  inf0  9606  dfom3  9632  dfac5lem4  10186  dfac9  10196  cflem  10304  canthp1lem2  10719  addsrpr  11141  mulsrpr  11142  trclublem  15128  gcdaddmlem  16676  tgjustf  28917  sto1i  32820  stji1i  32826  kur14lem9  35948  dfon2lem4  36518  dfttc3gw  37281  rtrclex  44576  comptiunov2i  44665