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

Theorem simplr3 1032
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr3  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )

Proof of Theorem simplr3
StepHypRef Expression
1 simpr3 996 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantr 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
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  5348  frfi  7671  wemappo  7877  iccsplit  11538  ccatswrd  12471  pcdvdstr  14063  vdwlem12  14174  cshwsidrepswmod0  14242  iscatd2  14741  oppccomfpropd  14788  resssetc  15082  resscatc  15095  yonedalem4c  15209  mod1ile  15397  mod2ile  15398  prdsmndd  15576  grprcan  15693  mulgnn0dir  15772  mulgdir  15774  mulgass  15779  mulgnn0di  16437  mulgdi  16438  dprd2da  16666  lmodprop2d  17133  lssintcl  17171  prdslmodd  17176  islmhm2  17245  islbs2  17361  islbs3  17362  mdetmul  18564  restopnb  18914  iuncon  19167  1stcelcls  19200  blsscls2  20214  stdbdbl  20227  xrsblre  20523  icccmplem2  20535  itg1val2  21298  cvxcl  22514  colline  23197  tglowdim2ln  23199  f1otrg  23289  f1otrge  23290  ax5seglem4  23350  ax5seglem5  23351  axcontlem3  23384  axcontlem8  23389  axcontlem9  23390  eengtrkg  23403  xrofsup  26226  submomnd  26338  ogrpaddltbi  26347  erdszelem8  27250  rescon  27299  cvmliftmolem2  27335  cvmlift2lem12  27367  broutsideof3  28321  outsideoftr  28324  outsidele  28327  dgrsub2  29659  el2wlksotot  30569  ply1mulgsumlem2  31019  dmatmul  31075  ltltncvr  33425  atcvrj2b  33434  cvrat4  33445  cvrat42  33446  2at0mat0  33527  islpln2a  33550  paddasslem11  33832  pmod1i  33850  lhpm0atN  34031  lautcvr  34094  cdlemg4c  34614  tendoplass  34785  tendodi1  34786  tendodi2  34787
  Copyright terms: Public domain W3C validator