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

Theorem simplr2 1001
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 965 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantr 453 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  soltmin  5275  frfi  7354  wemappo  7520  iccsplit  11031  ccatswrd  11775  pcdvdstr  13251  vdwlem12  13362  iscatd2  13908  oppccomfpropd  13955  resssetc  14249  resscatc  14262  mod1ile  14536  mod2ile  14537  prdsmndd  14730  grprcan  14840  mulgnn0dir  14915  mulgnn0di  15450  mulgdi  15451  lmodprop2d  16008  lssintcl  16042  prdslmodd  16047  islmhm2  16116  islbs3  16229  restopnb  17241  nrmsep  17423  iuncon  17493  ptpjopn  17646  blsscls2  18536  xrsblre  18844  icccmplem2  18856  icccvx  18977  xrofsup  24128  ofldaddlt  24243  erdszelem8  24886  cvmliftmolem2  24971  cvmlift2lem12  25003  ax5seglem5  25874  axcontlem3  25907  axcontlem4  25908  axcontlem8  25912  btwnswapid  25953  btwnsegle  26053  broutsideof3  26062  outsidele  26068  mendlmod  27480  mendassa  27481  stoweidlem60  27787  el2wlkonotot0  28392  cvrletrN  30133  ltltncvr  30282  atcvrj2b  30291  cvrat4  30302  2at0mat0  30384  islpln2a  30407  paddasslem11  30689  pmod1i  30707  lautcvr  30951  cdlemg4c  31471  tendoplass  31642  tendodi1  31643  tendodi2  31644
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator