Theorem mpanr1 713

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanr1.1	⊢ 𝜓
mpanr1.2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 ⊢ 𝜓
2		mpanr1.2	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	anassrs 471	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 711	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mpanr12  715  oacl  8498  omcl  8499  oaordi  8509  oawordri  8513  oaass  8524  oarec  8525  omordi  8529  omwordri  8535  odi  8542  omass  8543  oeoelem  8562  undom  9031  fimax2g  9224  fimin2g  9439  frr1  9711  axcnre  11116  divdiv23zi  11938  recp1lt1  12084  divgt0i  12094  divge0i  12095  ltreci  12096  lereci  12097  lt2msqi  12098  le2msqi  12099  msq11i  12100  ltdiv23i  12110  ltdivp1i  12112  zmin  12939  ge0gtmnf  13169  hashprg  14402  sqrt11i  15403  sqrtmuli  15404  sqrtmsq2i  15406  sqrtlei  15407  sqrtlti  15408  cos01gt0  16214  wspthsnwspthsnon  30073  vc2OLD  30728  vc0  30734  vcm  30736  nvpi  30827  nvge0  30833  ipval3  30869  ipidsq  30870  sspmval  30893  opsqrlem1  32300  opsqrlem6  32305  hstle  32390  hstrbi  32426  atordi  32544  weiunlem  36784  finorwe  37837  poimirlem6  38086  poimirlem7  38087  poimirlem16  38096  poimirlem19  38099  poimirlem20  38100