Theorem mpanr12 429

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 427	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 415	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  cnvoprab  5875  2dom  6308  phplem4  6341  mulidnq  6579  nq0m0r  6646  nq0a0  6647  addpinq1  6654  0idsr  6944  1idsr  6945  00sr  6946  addresr  7005  mulresr  7006  pitonnlem2  7015  ax0id  7044  recexaplem2  7742  reclt1  7974  crap0  8035  nominpos  8268  expnass  9580  crim  9745  sqrt00  9926  mulcn2  10151  opoe  10295