Theorem mpanr1 702

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 700	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 210  df-an 400

This theorem is referenced by:  mpanr12  704  oacl  8143  omcl  8144  oaordi  8155  oawordri  8159  oaass  8170  oarec  8171  omordi  8175  omwordri  8181  odi  8188  omass  8189  oeoelem  8207  fimax2g  8748  fimin2g  8945  axcnre  10575  divdiv23zi  11382  recp1lt1  11527  divgt0i  11537  divge0i  11538  ltreci  11539  lereci  11540  lt2msqi  11541  le2msqi  11542  msq11i  11543  ltdiv23i  11553  ltdivp1i  11555  zmin  12332  ge0gtmnf  12553  hashprg  13752  sqrt11i  14736  sqrtmuli  14737  sqrtmsq2i  14739  sqrtlei  14740  sqrtlti  14741  cos01gt0  15536  wspthsnwspthsnon  27702  vc2OLD  28351  vc0  28357  vcm  28359  nvpi  28450  nvge0  28456  ipval3  28492  ipidsq  28493  sspmval  28516  opsqrlem1  29923  opsqrlem6  29928  hstle  30013  hstrbi  30049  atordi  30167  frr1  33257  finorwe  34799  poimirlem6  35063  poimirlem7  35064  poimirlem16  35073  poimirlem19  35076  poimirlem20  35077