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  6234  2dom  6804  phplem4  6854  fiintim  6927  mulidnq  7387  nq0m0r  7454  nq0a0  7455  addpinq1  7462  0idsr  7765  1idsr  7766  00sr  7767  addresr  7835  mulresr  7836  pitonnlem2  7845  ax0id  7876  recexaplem2  8607  reclt1  8851  crap0  8913  nominpos  9154  expnass  10622  crim  10862  sqrt00  11044  mulcn2  11315  sin02gt0  11766  opoe  11894  oddprm  12253  pythagtriplem3  12261  pc1  12299  txswaphmeo  13714  sinq34lt0t  14145  cosordlem  14163  lgsne0  14332  lgsdinn0  14342