Theorem mpanr12 436

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 434	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 422	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  cnvoprab  6139  2dom  6707  phplem4  6757  fiintim  6825  mulidnq  7221  nq0m0r  7288  nq0a0  7289  addpinq1  7296  0idsr  7599  1idsr  7600  00sr  7601  addresr  7669  mulresr  7670  pitonnlem2  7679  ax0id  7710  recexaplem2  8437  reclt1  8678  crap0  8740  nominpos  8981  expnass  10429  crim  10662  sqrt00  10844  mulcn2  11113  sin02gt0  11506  opoe  11628  txswaphmeo  12529  sinq34lt0t  12960  cosordlem  12978