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  8608  reclt1  8852  crap0  8914  nominpos  9155  expnass  10625  crim  10866  sqrt00  11048  mulcn2  11319  sin02gt0  11770  opoe  11899  oddprm  12258  pythagtriplem3  12266  pc1  12304  txswaphmeo  13791  sinq34lt0t  14222  cosordlem  14240  lgsne0  14409  lgsdinn0  14419