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

Theorem simplr3 999
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 963 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  soltmin  5098  frfi  7118  wemappo  7280  iccsplit  10784  ccatswrd  11475  pcdvdstr  12944  vdwlem12  13055  iscatd2  13599  oppccomfpropd  13646  resssetc  13940  resscatc  13953  yonedalem4c  14067  mod1ile  14227  mod2ile  14228  prdsmndd  14421  grprcan  14531  mulgnn0dir  14606  mulgdir  14608  mulgass  14613  mulgnn0di  15141  mulgdi  15142  dprd2da  15293  lmodprop2d  15703  lssintcl  15737  prdslmodd  15742  islmhm2  15811  islbs2  15923  islbs3  15924  restopnb  16922  iuncon  17170  1stcelcls  17203  blsscls2  18066  stdbdbl  18079  xrsblre  18333  icccmplem2  18344  itg1val2  19055  cvxcl  20295  xrofsup  23270  erdszelem8  23744  rescon  23792  cvmliftmolem2  23828  cvmlift2lem12  23860  ax5seglem4  24632  ax5seglem5  24633  axcontlem3  24666  axcontlem8  24671  axcontlem9  24672  broutsideof3  24821  outsideoftr  24824  outsidele  24827  lvsovso3  25731  addcanrg  25770  icccon2  25803  dgrsub2  27442  ltltncvr  30234  atcvrj2b  30243  cvrat4  30254  cvrat42  30255  2at0mat0  30336  islpln2a  30359  paddasslem11  30641  pmod1i  30659  lhpm0atN  30840  lautcvr  30903  cdlemg4c  31423  tendoplass  31594  tendodi1  31595  tendodi2  31596
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator