Theorem mpanr12 439

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  cnvoprab  6443  2dom  7059  phplem4  7122  fiintim  7204  mulidnq  7720  nq0m0r  7787  nq0a0  7788  addpinq1  7795  0idsr  8098  1idsr  8099  00sr  8100  addresr  8168  mulresr  8169  pitonnlem2  8178  ax0id  8209  recexaplem2  8943  reclt1  9187  crap0  9249  nominpos  9493  expnass  11031  crim  11568  sqrt00  11750  mulcn2  12022  sin02gt0  12475  opoe  12606  oddprm  12982  pythagtriplem3  12990  pc1  13028  txswaphmeo  15298  sinq34lt0t  15808  cosordlem  15826  lgsne0  16023  lgsdinn0  16033  eupth2lem3lem4fi  16580  3dom  16874