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

Theorem mpanr1 666
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 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 664 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpanr12  668  oacl  6781  omcl  6782  oaordi  6791  oawordri  6795  oaass  6806  oarec  6807  omordi  6811  omwordri  6817  odi  6824  omass  6825  oeoelem  6843  fimax2g  7355  noinfepOLD  7617  axcnre  9041  divdiv23zi  9769  recp1lt1  9910  divgt0i  9921  divge0i  9922  ltreci  9923  lereci  9924  lt2msqi  9925  le2msqi  9926  msq11i  9927  ltdiv23i  9937  ltdivp1i  9939  zmin  10572  ge0gtmnf  10762  hashprg  11668  sqr11i  12190  sqrmuli  12191  sqrmsq2i  12193  sqrlei  12194  sqrlti  12195  cos01gt0  12794  0wlk  21547  0trl  21548  0pth  21572  0spth  21573  0crct  21615  0cycl  21616  vc2  22036  vc0  22050  vcm  22052  vcnegneg  22055  nvnncan  22146  nvpi  22157  nvge0  22165  ipval3  22207  ipidsq  22211  sspmval  22234  opsqrlem1  23645  opsqrlem6  23650  hstle  23735  hstrbi  23771  atordi  23889
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 179  df-an 362
  Copyright terms: Public domain W3C validator