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  6534  omcl  6535  oaordi  6544  oawordri  6548  oaass  6559  oarec  6560  omordi  6564  omwordri  6570  odi  6577  omass  6578  oeoelem  6596  fimax2g  7103  noinfepOLD  7361  axcnre  8786  divdiv23zi  9513  recp1lt1  9654  divgt0i  9665  divge0i  9666  ltreci  9667  lereci  9668  lt2msqi  9669  le2msqi  9670  msq11i  9671  ltdiv23i  9681  ltdivp1i  9683  zmin  10312  ge0gtmnf  10501  hashprg  11368  sqr11i  11868  sqrmuli  11869  sqrmsq2i  11871  sqrlei  11872  sqrlti  11873  cos01gt0  12471  vc2  21111  vc0  21125  vcm  21127  vcnegneg  21130  nvnncan  21221  nvpi  21232  nvge0  21240  ipval3  21282  ipidsq  21286  sspmval  21309  opsqrlem1  22720  opsqrlem6  22725  hstle  22810  hstrbi  22846  atordi  22964
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