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  6443  2dom  7059  phplem4  7122  fiintim  7204  mulidnq  7720  nq0m0r  7787  nq0a0  7788  addpinq1  7795  0idsr  8098  1idsr  8099  00sr  8100  addresr  8168  mulresr  8169  pitonnlem2  8178  ax0id  8209  recexaplem2  8944  reclt1  9190  crap0  9252  nominpos  9496  expnass  11034  crim  11571  sqrt00  11754  mulcn2  12026  sin02gt0  12479  opoe  12610  oddprm  12986  pythagtriplem3  12994  pc1  13032  txswaphmeo  15316  sinq34lt0t  15826  cosordlem  15844  lgsne0  16041  lgsdinn0  16051  eupth2lem3lem4fi  16598  3dom  16902