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

Theorem simplr2 1039
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 1003 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantr 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  soltmin  5404  frfi  7761  wemappo  7970  iccsplit  11649  ccatswrd  12640  pcdvdstr  14254  vdwlem12  14365  iscatd2  14932  oppccomfpropd  14979  resssetc  15273  resscatc  15286  mod1ile  15588  mod2ile  15589  prdsmndd  15767  grprcan  15884  mulgnn0dir  15965  mulgnn0di  16630  mulgdi  16631  lmodprop2d  17355  lssintcl  17393  prdslmodd  17398  islmhm2  17467  islbs3  17584  mdetmul  18892  restopnb  19442  nrmsep  19624  iuncon  19695  ptpjopn  19848  blsscls2  20742  xrsblre  21051  icccmplem2  21063  icccvx  21185  colline  23743  tglowdim2ln  23745  f1otrg  23850  f1otrge  23851  ax5seglem5  23912  axcontlem3  23945  axcontlem4  23946  axcontlem8  23950  eengtrkg  23964  erclwwlktr  24491  erclwwlkntr  24503  el2wlkonotot0  24548  xrofsup  27250  submomnd  27362  ogrpaddltbi  27371  erdszelem8  28282  cvmliftmolem2  28367  cvmlift2lem12  28399  btwnswapid  29244  btwnsegle  29344  broutsideof3  29353  outsidele  29359  mendlmod  30747  mendassa  30748  3adantlr3  30995  ioondisj2  31089  ioondisj1  31090  stoweidlem60  31360  ply1mulgsumlem2  32060  lincresunit3lem2  32154  cvrletrN  34070  ltltncvr  34219  atcvrj2b  34228  cvrat4  34239  2at0mat0  34321  islpln2a  34344  paddasslem11  34626  pmod1i  34644  lautcvr  34888  cdlemg4c  35408  tendoplass  35579  tendodi1  35580  tendodi2  35581
  Copyright terms: Public domain W3C validator