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

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
StepHypRef Expression
1 mpanr1.1 . 2 𝜓
2 mpanr1.2 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32anassrs 471 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 700 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
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  8150  omcl  8151  oaordi  8162  oawordri  8166  oaass  8177  oarec  8178  omordi  8182  omwordri  8188  odi  8195  omass  8196  oeoelem  8214  fimax2g  8755  fimin2g  8952  axcnre  10578  divdiv23zi  11385  recp1lt1  11530  divgt0i  11540  divge0i  11541  ltreci  11542  lereci  11543  lt2msqi  11544  le2msqi  11545  msq11i  11546  ltdiv23i  11556  ltdivp1i  11558  zmin  12337  ge0gtmnf  12558  hashprg  13757  sqrt11i  14740  sqrtmuli  14741  sqrtmsq2i  14743  sqrtlei  14744  sqrtlti  14745  cos01gt0  15540  wspthsnwspthsnon  27698  vc2OLD  28347  vc0  28353  vcm  28355  nvpi  28446  nvge0  28452  ipval3  28488  ipidsq  28489  sspmval  28512  opsqrlem1  29919  opsqrlem6  29924  hstle  30009  hstrbi  30045  atordi  30163  frr1  33169  finorwe  34711  poimirlem6  34973  poimirlem7  34974  poimirlem16  34983  poimirlem19  34986  poimirlem20  34987
  Copyright terms: Public domain W3C validator