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  6576  omcl  6577  oaordi  6586  oawordri  6590  oaass  6601  oarec  6602  omordi  6606  omwordri  6612  odi  6619  omass  6620  oeoelem  6638  fimax2g  7148  noinfepOLD  7406  axcnre  8831  divdiv23zi  9558  recp1lt1  9699  divgt0i  9710  divge0i  9711  ltreci  9712  lereci  9713  lt2msqi  9714  le2msqi  9715  msq11i  9716  ltdiv23i  9726  ltdivp1i  9728  zmin  10359  ge0gtmnf  10548  hashprg  11415  sqr11i  11915  sqrmuli  11916  sqrmsq2i  11918  sqrlei  11919  sqrlti  11920  cos01gt0  12518  vc2  21166  vc0  21180  vcm  21182  vcnegneg  21185  nvnncan  21276  nvpi  21287  nvge0  21295  ipval3  21337  ipidsq  21341  sspmval  21364  opsqrlem1  22775  opsqrlem6  22780  hstle  22865  hstrbi  22901  atordi  23019  0wlk  27457  0trl  27458  0pth  27472  0spth  27473  0crct  27509  0cycl  27510
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