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  6230  2dom  6800  phplem4  6850  fiintim  6923  mulidnq  7383  nq0m0r  7450  nq0a0  7451  addpinq1  7458  0idsr  7761  1idsr  7762  00sr  7763  addresr  7831  mulresr  7832  pitonnlem2  7841  ax0id  7872  recexaplem2  8603  reclt1  8847  crap0  8909  nominpos  9150  expnass  10618  crim  10858  sqrt00  11040  mulcn2  11311  sin02gt0  11762  opoe  11890  oddprm  12249  pythagtriplem3  12257  pc1  12295  txswaphmeo  13603  sinq34lt0t  14034  cosordlem  14052  lgsne0  14221  lgsdinn0  14231