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

Theorem simplr3 1041
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 1005 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantr 463 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ 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 369  df-3an 976
This theorem is referenced by:  soltmin  5223  frfi  7798  wemappo  8007  iccsplit  11705  ccatswrd  12735  swrdccat3  12771  pcdvdstr  14606  vdwlem12  14717  cshwsidrepswmod0  14786  iscatd2  15293  oppccomfpropd  15338  initoeu2lem0  15614  resssetc  15693  resscatc  15706  yonedalem4c  15868  mod1ile  16057  mod2ile  16058  prdsmndd  16275  grprcan  16405  mulgnn0dir  16487  mulgdir  16489  mulgass  16494  mulgnn0di  17156  mulgdi  17157  dprd2da  17409  lmodprop2d  17890  lssintcl  17928  prdslmodd  17933  islmhm2  18002  islbs2  18118  islbs3  18119  dmatmul  19289  mdetmul  19415  restopnb  19967  iuncon  20219  1stcelcls  20252  blsscls2  21297  stdbdbl  21310  xrsblre  21606  icccmplem2  21618  itg1val2  22381  cvxcl  23638  colline  24413  tglowdim2ln  24415  f1otrg  24578  f1otrge  24579  ax5seglem4  24639  ax5seglem5  24640  axcontlem3  24673  axcontlem8  24678  axcontlem9  24679  eengtrkg  24692  el2wlksotot  25286  xrofsup  28016  submomnd  28138  ogrpaddltbi  28147  erdszelem8  29482  rescon  29530  cvmliftmolem2  29566  cvmlift2lem12  29598  broutsideof3  30451  outsideoftr  30454  outsidele  30457  ltltncvr  32420  atcvrj2b  32429  cvrat4  32440  cvrat42  32441  2at0mat0  32522  islpln2a  32545  paddasslem11  32827  pmod1i  32845  lhpm0atN  33026  lautcvr  33089  cdlemg4c  33611  tendoplass  33782  tendodi1  33783  tendodi2  33784  dgrsub2  35428  ioondisj2  36874  ioondisj1  36875  pfxccat3  37894  ply1mulgsumlem2  38479
  Copyright terms: Public domain W3C validator