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  6332  2dom  6910  phplem4  6966  fiintim  7042  mulidnq  7517  nq0m0r  7584  nq0a0  7585  addpinq1  7592  0idsr  7895  1idsr  7896  00sr  7897  addresr  7965  mulresr  7966  pitonnlem2  7975  ax0id  8006  recexaplem2  8740  reclt1  8984  crap0  9046  nominpos  9290  expnass  10807  crim  11239  sqrt00  11421  mulcn2  11693  sin02gt0  12145  opoe  12276  oddprm  12652  pythagtriplem3  12660  pc1  12698  txswaphmeo  14863  sinq34lt0t  15373  cosordlem  15391  lgsne0  15585  lgsdinn0  15595