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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  cnvoprab  6470  2dom  7093  phplem4  7156  fiintim  7238  mulidnq  7757  nq0m0r  7824  nq0a0  7825  addpinq1  7832  0idsr  8135  1idsr  8136  00sr  8137  addresr  8205  mulresr  8206  pitonnlem2  8215  ax0id  8246  recexaplem2  8983  reclt1  9229  crap0  9291  nominpos  9548  expnass  11096  crim  11638  sqrt00  11821  mulcn2  12096  sin02gt0  12549  opoe  12680  oddprm  13060  pythagtriplem3  13068  pc1  13106  prmlem0  13242  txswaphmeo  15474  sinq34lt0t  15985  cosordlem  16003  ppiqub  16215  lgsne0  16279  lgsdinn0  16289  eupth2lem3lem4fi  16836  3dom  17140