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

Theorem mpanr1 665
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 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 663 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanr12  667  oacl  6771  omcl  6772  oaordi  6781  oawordri  6785  oaass  6796  oarec  6797  omordi  6801  omwordri  6807  odi  6814  omass  6815  oeoelem  6833  fimax2g  7345  noinfepOLD  7607  axcnre  9031  divdiv23zi  9759  recp1lt1  9900  divgt0i  9911  divge0i  9912  ltreci  9913  lereci  9914  lt2msqi  9915  le2msqi  9916  msq11i  9917  ltdiv23i  9927  ltdivp1i  9929  zmin  10562  ge0gtmnf  10752  hashprg  11658  sqr11i  12180  sqrmuli  12181  sqrmsq2i  12183  sqrlei  12184  sqrlti  12185  cos01gt0  12784  0wlk  21537  0trl  21538  0pth  21562  0spth  21563  0crct  21605  0cycl  21606  vc2  22026  vc0  22040  vcm  22042  vcnegneg  22045  nvnncan  22136  nvpi  22147  nvge0  22155  ipval3  22197  ipidsq  22201  sspmval  22224  opsqrlem1  23635  opsqrlem6  23640  hstle  23725  hstrbi  23761  atordi  23879
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 178  df-an 361
  Copyright terms: Public domain W3C validator