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

Theorem simplr2 1031
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 995 . 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 965
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 967
This theorem is referenced by:  soltmin  5237  frfi  7557  wemappo  7763  iccsplit  11418  ccatswrd  12350  pcdvdstr  13942  vdwlem12  14053  iscatd2  14619  oppccomfpropd  14666  resssetc  14960  resscatc  14973  mod1ile  15275  mod2ile  15276  prdsmndd  15454  grprcan  15571  mulgnn0dir  15650  mulgnn0di  16313  mulgdi  16314  lmodprop2d  17007  lssintcl  17045  prdslmodd  17050  islmhm2  17119  islbs3  17236  mdetmul  18429  restopnb  18779  nrmsep  18961  iuncon  19032  ptpjopn  19185  blsscls2  20079  xrsblre  20388  icccmplem2  20400  icccvx  20522  colline  23052  f1otrg  23117  f1otrge  23118  ax5seglem5  23179  axcontlem3  23212  axcontlem4  23213  axcontlem8  23217  eengtrkg  23231  xrofsup  26055  submomnd  26173  ogrpaddltbi  26182  erdszelem8  27086  cvmliftmolem2  27171  cvmlift2lem12  27203  btwnswapid  28048  btwnsegle  28148  broutsideof3  28157  outsidele  28163  mendlmod  29550  mendassa  29551  stoweidlem60  29855  el2wlkonotot0  30391  erclwwlktr  30485  erclwwlkntr  30501  ply1mulgsumlem2  30845  lincresunit3lem2  31014  cvrletrN  32918  ltltncvr  33067  atcvrj2b  33076  cvrat4  33087  2at0mat0  33169  islpln2a  33192  paddasslem11  33474  pmod1i  33492  lautcvr  33736  cdlemg4c  34256  tendoplass  34427  tendodi1  34428  tendodi2  34429
  Copyright terms: Public domain W3C validator