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

Theorem mpanr1 664
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 629 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 662 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanr12  666  oacl  6550  omcl  6551  oaordi  6560  oawordri  6564  oaass  6575  oarec  6576  omordi  6580  omwordri  6586  odi  6593  omass  6594  oeoelem  6612  fimax2g  7119  noinfepOLD  7377  axcnre  8802  divdiv23zi  9529  recp1lt1  9670  divgt0i  9681  divge0i  9682  ltreci  9683  lereci  9684  lt2msqi  9685  le2msqi  9686  msq11i  9687  ltdiv23i  9697  ltdivp1i  9699  zmin  10328  ge0gtmnf  10517  hashprg  11384  sqr11i  11884  sqrmuli  11885  sqrmsq2i  11887  sqrlei  11888  sqrlti  11889  cos01gt0  12487  vc2  21127  vc0  21141  vcm  21143  vcnegneg  21146  nvnncan  21237  nvpi  21248  nvge0  21256  ipval3  21298  ipidsq  21302  sspmval  21325  opsqrlem1  22736  opsqrlem6  22741  hstle  22826  hstrbi  22862  atordi  22980  0wlk  28343  0trl  28344  0pth  28356  0spth  28357  0crct  28371  0cycl  28372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator