Theorem mpanr12 435

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 433	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 421	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  6131  2dom  6699  phplem4  6749  fiintim  6817  mulidnq  7197  nq0m0r  7264  nq0a0  7265  addpinq1  7272  0idsr  7575  1idsr  7576  00sr  7577  addresr  7645  mulresr  7646  pitonnlem2  7655  ax0id  7686  recexaplem2  8413  reclt1  8654  crap0  8716  nominpos  8957  expnass  10398  crim  10630  sqrt00  10812  mulcn2  11081  sin02gt0  11470  opoe  11592  txswaphmeo  12490  sinq34lt0t  12912  cosordlem  12930