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  5098  frfi  7118  wemappo  7280  iccsplit  10784  ccatswrd  11475  pcdvdstr  12944  vdwlem12  13055  iscatd2  13599  oppccomfpropd  13646  resssetc  13940  resscatc  13953  mod1ile  14227  mod2ile  14228  prdsmndd  14421  grprcan  14531  mulgnn0dir  14606  mulgnn0di  15141  mulgdi  15142  lmodprop2d  15703  lssintcl  15737  prdslmodd  15742  islmhm2  15811  islbs3  15924  restopnb  16922  nrmsep  17101  iuncon  17170  ptpjopn  17322  blsscls2  18066  xrsblre  18333  icccmplem2  18344  icccvx  18464  xrofsup  23270  erdszelem8  23744  cvmliftmolem2  23828  cvmlift2lem12  23860  ax5seglem5  24633  axcontlem3  24666  axcontlem4  24667  axcontlem8  24671  btwnswapid  24712  btwnsegle  24812  broutsideof3  24821  outsidele  24827  addcanrg  25770  mendlmod  27604  mendassa  27605  stoweidlem60  27912  cvrletrN  30085  ltltncvr  30234  atcvrj2b  30243  cvrat4  30254  2at0mat0  30336  islpln2a  30359  paddasslem11  30641  pmod1i  30659  lautcvr  30903  cdlemg4c  31423  tendoplass  31594  tendodi1  31595  tendodi2  31596
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