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  6408  2dom  7023  phplem4  7084  fiintim  7166  mulidnq  7652  nq0m0r  7719  nq0a0  7720  addpinq1  7727  0idsr  8030  1idsr  8031  00sr  8032  addresr  8100  mulresr  8101  pitonnlem2  8110  ax0id  8141  recexaplem2  8875  reclt1  9119  crap0  9181  nominpos  9425  expnass  10951  crim  11479  sqrt00  11661  mulcn2  11933  sin02gt0  12386  opoe  12517  oddprm  12893  pythagtriplem3  12901  pc1  12939  txswaphmeo  15112  sinq34lt0t  15622  cosordlem  15640  lgsne0  15837  lgsdinn0  15847  eupth2lem3lem4fi  16394  3dom  16688