MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanr1 Structured version   Visualization version   GIF version

Theorem mpanr1 699
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
StepHypRef Expression
1 mpanr1.1 . 2 𝜓
2 mpanr1.2 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32anassrs 468 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 697 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpanr12  701  oacl  8149  omcl  8150  oaordi  8161  oawordri  8165  oaass  8176  oarec  8177  omordi  8181  omwordri  8187  odi  8194  omass  8195  oeoelem  8213  fimax2g  8752  fimin2g  8949  axcnre  10574  divdiv23zi  11381  recp1lt1  11526  divgt0i  11536  divge0i  11537  ltreci  11538  lereci  11539  lt2msqi  11540  le2msqi  11541  msq11i  11542  ltdiv23i  11552  ltdivp1i  11554  zmin  12332  ge0gtmnf  12553  hashprg  13744  sqrt11i  14732  sqrtmuli  14733  sqrtmsq2i  14735  sqrtlei  14736  sqrtlti  14737  cos01gt0  15532  wspthsnwspthsnon  27622  vc2OLD  28272  vc0  28278  vcm  28280  nvpi  28371  nvge0  28377  ipval3  28413  ipidsq  28414  sspmval  28437  opsqrlem1  29844  opsqrlem6  29849  hstle  29934  hstrbi  29970  atordi  30088  frr1  33041  finorwe  34545  poimirlem6  34779  poimirlem7  34780  poimirlem16  34789  poimirlem19  34792  poimirlem20  34793
  Copyright terms: Public domain W3C validator