Theorem mpanr12 431

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

Ref	Expression
mpanr12.1	⊢ 𝜓
mpanr12.2	⊢ 𝜒
mpanr12.3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 429	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 417	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  cnvoprab  6013  2dom  6576  phplem4  6625  fiintim  6693  mulidnq  7009  nq0m0r  7076  nq0a0  7077  addpinq1  7084  0idsr  7374  1idsr  7375  00sr  7376  addresr  7435  mulresr  7436  pitonnlem2  7445  ax0id  7474  recexaplem2  8182  reclt1  8418  crap0  8479  nominpos  8714  expnass  10121  crim  10353  sqrt00  10534  mulcn2  10762  sin02gt0  11115  opoe  11234