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  6474  2dom  7099  phplem4  7162  fiintim  7244  mulidnq  7763  nq0m0r  7830  nq0a0  7831  addpinq1  7838  0idsr  8141  1idsr  8142  00sr  8143  addresr  8211  mulresr  8212  pitonnlem2  8221  ax0id  8252  recexaplem2  8989  reclt1  9235  crap0  9297  nominpos  9555  expnass  11103  crim  11645  sqrt00  11828  mulcn2  12103  sin02gt0  12556  opoe  12687  oddprm  13067  pythagtriplem3  13075  pc1  13113  prmlem0  13249  txswaphmeo  15580  sinq34lt0t  16091  cosordlem  16110  ppiqub  16326  bposlem9  16352  lgsne0  16395  lgsdinn0  16405  eupth2lem3lem4fi  16952  3dom  17256