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

Theorem simplr2 1040
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 1004 . 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 974
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 976
This theorem is referenced by:  soltmin  5396  frfi  7767  wemappo  7977  iccsplit  11664  ccatswrd  12663  pcdvdstr  14381  vdwlem12  14492  iscatd2  15060  oppccomfpropd  15104  resssetc  15398  resscatc  15411  mod1ile  15714  mod2ile  15715  prdsmndd  15932  grprcan  16062  mulgnn0dir  16144  mulgnn0di  16813  mulgdi  16814  lmodprop2d  17551  lssintcl  17589  prdslmodd  17594  islmhm2  17663  islbs3  17780  mdetmul  19103  restopnb  19654  nrmsep  19836  iuncon  19907  ptpjopn  20091  blsscls2  20985  xrsblre  21294  icccmplem2  21306  icccvx  21428  colline  24008  tglowdim2ln  24010  f1otrg  24152  f1otrge  24153  ax5seglem5  24214  axcontlem3  24247  axcontlem4  24248  axcontlem8  24252  eengtrkg  24266  erclwwlktr  24793  erclwwlkntr  24805  el2wlkonotot0  24850  extwwlkfablem1  25052  xrofsup  27560  submomnd  27678  ogrpaddltbi  27687  erdszelem8  28620  cvmliftmolem2  28705  cvmlift2lem12  28737  btwnswapid  29643  btwnsegle  29743  broutsideof3  29752  outsidele  29758  mendlmod  31118  mendassa  31119  3adantlr3  31371  ioondisj2  31479  ioondisj1  31480  stoweidlem60  31796  ply1mulgsumlem2  32857  lincresunit3lem2  32951  cvrletrN  34873  ltltncvr  35022  atcvrj2b  35031  cvrat4  35042  2at0mat0  35124  islpln2a  35147  paddasslem11  35429  pmod1i  35447  lautcvr  35691  cdlemg4c  36213  tendoplass  36384  tendodi1  36385  tendodi2  36386
  Copyright terms: Public domain W3C validator