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 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
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  swrdccat3  12699  pcdvdstr  14381  vdwlem12  14492  cshwsidrepswmod0  14561  iscatd2  15060  oppccomfpropd  15104  resssetc  15398  resscatc  15411  yonedalem4c  15525  mod1ile  15714  mod2ile  15715  prdsmndd  15932  grprcan  16062  mulgnn0dir  16144  mulgdir  16146  mulgass  16151  mulgnn0di  16813  mulgdi  16814  dprd2da  17070  lmodprop2d  17551  lssintcl  17589  prdslmodd  17594  islmhm2  17663  islbs2  17779  islbs3  17780  dmatmul  18977  mdetmul  19103  restopnb  19654  iuncon  19907  1stcelcls  19940  blsscls2  20985  stdbdbl  20998  xrsblre  21294  icccmplem2  21306  itg1val2  22069  cvxcl  23292  colline  24008  tglowdim2ln  24010  f1otrg  24152  f1otrge  24153  ax5seglem4  24213  ax5seglem5  24214  axcontlem3  24247  axcontlem8  24252  axcontlem9  24253  eengtrkg  24266  el2wlksotot  24860  xrofsup  27560  submomnd  27678  ogrpaddltbi  27687  erdszelem8  28620  rescon  28669  cvmliftmolem2  28705  cvmlift2lem12  28737  broutsideof3  29752  outsideoftr  29755  outsidele  29758  dgrsub2  31060  ioondisj2  31479  ioondisj1  31480  ply1mulgsumlem2  32857  ltltncvr  35022  atcvrj2b  35031  cvrat4  35042  cvrat42  35043  2at0mat0  35124  islpln2a  35147  paddasslem11  35429  pmod1i  35447  lhpm0atN  35628  lautcvr  35691  cdlemg4c  36213  tendoplass  36384  tendodi1  36385  tendodi2  36386
  Copyright terms: Public domain W3C validator