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  11423  sqrt00  11605  mulcn2  11877  sin02gt0  12330  opoe  12461  oddprm  12837  pythagtriplem3  12845  pc1  12883  txswaphmeo  15051  sinq34lt0t  15561  cosordlem  15579  lgsne0  15773  lgsdinn0  15783  eupth2lem3lem4fi  16330  3dom  16613