Theorem mpanr12 443

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 441	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 429	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  6464  2dom  7087  phplem4  7150  fiintim  7232  mulidnq  7750  nq0m0r  7817  nq0a0  7818  addpinq1  7825  0idsr  8128  1idsr  8129  00sr  8130  addresr  8198  mulresr  8199  pitonnlem2  8208  ax0id  8239  recexaplem2  8974  reclt1  9220  crap0  9282  nominpos  9526  expnass  11065  crim  11606  sqrt00  11789  mulcn2  12061  sin02gt0  12514  opoe  12645  oddprm  13021  pythagtriplem3  13029  pc1  13067  txswaphmeo  15405  sinq34lt0t  15915  cosordlem  15933  lgsne0  16140  lgsdinn0  16150  eupth2lem3lem4fi  16697  3dom  17001