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  6394  2dom  6975  phplem4  7036  fiintim  7118  mulidnq  7602  nq0m0r  7669  nq0a0  7670  addpinq1  7677  0idsr  7980  1idsr  7981  00sr  7982  addresr  8050  mulresr  8051  pitonnlem2  8060  ax0id  8091  recexaplem2  8825  reclt1  9069  crap0  9131  nominpos  9375  expnass  10900  crim  11412  sqrt00  11594  mulcn2  11866  sin02gt0  12318  opoe  12449  oddprm  12825  pythagtriplem3  12833  pc1  12871  txswaphmeo  15038  sinq34lt0t  15548  cosordlem  15566  lgsne0  15760  lgsdinn0  15770  3dom  16537