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

Theorem mpanr1 688
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  |-  ps
mpanr1.2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr1  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mpanr1
StepHypRef Expression
1 mpanr1.1 . 2  |-  ps
2 mpanr1.2 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32anassrs 653 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 686 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  mpanr12  690  oacl  7243  omcl  7244  oaordi  7253  oawordri  7257  oaass  7268  oarec  7269  omordi  7273  omwordri  7279  odi  7286  omass  7287  oeoelem  7305  fimax2g  7821  fimin2g  8017  axcnre  9590  divdiv23zi  10362  recp1lt1  10506  divgt0i  10517  divge0i  10518  ltreci  10519  lereci  10520  lt2msqi  10521  le2msqi  10522  msq11i  10523  ltdiv23i  10533  ltdivp1i  10535  zmin  11262  ge0gtmnf  11469  hashprg  12573  sqrt11i  13441  sqrtmuli  13442  sqrtmsq2i  13444  sqrtlei  13445  sqrtlti  13446  cos01gt0  14238  0wlk  25267  0trl  25268  0pth  25292  0spth  25293  0crct  25346  0cycl  25347  0clwlk  25485  vc2  26166  vc0  26180  vcm  26182  vcnegneg  26185  nvnncan  26276  nvpi  26287  nvge0  26295  ipval3  26337  ipidsq  26341  sspmval  26364  opsqrlem1  27785  opsqrlem6  27790  hstle  27875  hstrbi  27911  atordi  28029  poimirlem6  31904  poimirlem7  31905  poimirlem16  31914  poimirlem19  31917  poimirlem20  31918
  Copyright terms: Public domain W3C validator