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  7098  phplem4  7161  fiintim  7243  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  11104  crim  11646  sqrt00  11829  mulcn2  12104  sin02gt0  12557  opoe  12688  oddprm  13068  pythagtriplem3  13076  pc1  13114  prmlem0  13250  txswaphmeo  15559  sinq34lt0t  16070  cosordlem  16089  ppiqub  16305  bposlem9  16331  lgsne0  16374  lgsdinn0  16384  eupth2lem3lem4fi  16931  3dom  17235