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

Theorem simplr3 1001
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 965 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  soltmin  5273  frfi  7352  wemappo  7518  iccsplit  11029  ccatswrd  11773  pcdvdstr  13249  vdwlem12  13360  iscatd2  13906  oppccomfpropd  13953  resssetc  14247  resscatc  14260  yonedalem4c  14374  mod1ile  14534  mod2ile  14535  prdsmndd  14728  grprcan  14838  mulgnn0dir  14913  mulgdir  14915  mulgass  14920  mulgnn0di  15448  mulgdi  15449  dprd2da  15600  lmodprop2d  16006  lssintcl  16040  prdslmodd  16045  islmhm2  16114  islbs2  16226  islbs3  16227  restopnb  17239  iuncon  17491  1stcelcls  17524  blsscls2  18534  stdbdbl  18547  xrsblre  18842  icccmplem2  18854  itg1val2  19576  cvxcl  20823  xrofsup  24126  ofldaddlt  24241  erdszelem8  24884  rescon  24933  cvmliftmolem2  24969  cvmlift2lem12  25001  ax5seglem4  25871  ax5seglem5  25872  axcontlem3  25905  axcontlem8  25910  axcontlem9  25911  broutsideof3  26060  outsideoftr  26063  outsidele  26066  dgrsub2  27316  cshwidx  28242  el2wlksotot  28349  ltltncvr  30220  atcvrj2b  30229  cvrat4  30240  cvrat42  30241  2at0mat0  30322  islpln2a  30345  paddasslem11  30627  pmod1i  30645  lhpm0atN  30826  lautcvr  30889  cdlemg4c  31409  tendoplass  31580  tendodi1  31581  tendodi2  31582
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator