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

Theorem simplr2 998
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr2  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ps )

Proof of Theorem simplr2
StepHypRef Expression
1 simpr2 962 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  soltmin  5082  frfi  7102  wemappo  7264  iccsplit  10768  ccatswrd  11459  pcdvdstr  12928  vdwlem12  13039  iscatd2  13583  oppccomfpropd  13630  resssetc  13924  resscatc  13937  mod1ile  14211  mod2ile  14212  prdsmndd  14405  grprcan  14515  mulgnn0dir  14590  mulgnn0di  15125  mulgdi  15126  lmodprop2d  15687  lssintcl  15721  prdslmodd  15726  islmhm2  15795  islbs3  15908  restopnb  16906  nrmsep  17085  iuncon  17154  ptpjopn  17306  blsscls2  18050  xrsblre  18317  icccmplem2  18328  icccvx  18448  xrofsup  23255  erdszelem8  23729  cvmliftmolem2  23813  cvmlift2lem12  23845  ax5seglem5  24561  axcontlem3  24594  axcontlem4  24595  axcontlem8  24599  btwnswapid  24640  btwnsegle  24740  broutsideof3  24749  outsidele  24755  addcanrg  25667  mendlmod  27501  mendassa  27502  stoweidlem60  27809  cvrletrN  29463  ltltncvr  29612  atcvrj2b  29621  cvrat4  29632  2at0mat0  29714  islpln2a  29737  paddasslem11  30019  pmod1i  30037  lautcvr  30281  cdlemg4c  30801  tendoplass  30972  tendodi1  30973  tendodi2  30974
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  df-3an 936
  Copyright terms: Public domain W3C validator