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  6429  2dom  7045  phplem4  7108  fiintim  7190  mulidnq  7703  nq0m0r  7770  nq0a0  7771  addpinq1  7778  0idsr  8081  1idsr  8082  00sr  8083  addresr  8151  mulresr  8152  pitonnlem2  8161  ax0id  8192  recexaplem2  8925  reclt1  9169  crap0  9231  nominpos  9475  expnass  11006  crim  11539  sqrt00  11721  mulcn2  11993  sin02gt0  12446  opoe  12577  oddprm  12953  pythagtriplem3  12961  pc1  12999  txswaphmeo  15178  sinq34lt0t  15688  cosordlem  15706  lgsne0  15903  lgsdinn0  15913  eupth2lem3lem4fi  16460  3dom  16754