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  6399  2dom  6980  phplem4  7041  fiintim  7123  mulidnq  7609  nq0m0r  7676  nq0a0  7677  addpinq1  7684  0idsr  7987  1idsr  7988  00sr  7989  addresr  8057  mulresr  8058  pitonnlem2  8067  ax0id  8098  recexaplem2  8832  reclt1  9076  crap0  9138  nominpos  9382  expnass  10908  crim  11420  sqrt00  11602  mulcn2  11874  sin02gt0  12327  opoe  12458  oddprm  12834  pythagtriplem3  12842  pc1  12880  txswaphmeo  15048  sinq34lt0t  15558  cosordlem  15576  lgsne0  15770  lgsdinn0  15780  eupth2lem3lem4fi  16327  3dom  16608