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  6171  2dom  6739  phplem4  6789  fiintim  6862  mulidnq  7288  nq0m0r  7355  nq0a0  7356  addpinq1  7363  0idsr  7666  1idsr  7667  00sr  7668  addresr  7736  mulresr  7737  pitonnlem2  7746  ax0id  7777  recexaplem2  8505  reclt1  8746  crap0  8808  nominpos  9049  expnass  10502  crim  10735  sqrt00  10917  mulcn2  11186  sin02gt0  11637  opoe  11759  txswaphmeo  12660  sinq34lt0t  13091  cosordlem  13109