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  5082  frfi  7102  wemappo  7264  iccsplit  10768  ccatswrd  11459  pcdvdstr  12928  vdwlem12  13039  iscatd2  13583  oppccomfpropd  13630  resssetc  13924  resscatc  13937  yonedalem4c  14051  mod1ile  14211  mod2ile  14212  prdsmndd  14405  grprcan  14515  mulgnn0dir  14590  mulgdir  14592  mulgass  14597  mulgnn0di  15125  mulgdi  15126  dprd2da  15277  lmodprop2d  15687  lssintcl  15721  prdslmodd  15726  islmhm2  15795  islbs2  15907  islbs3  15908  restopnb  16906  iuncon  17154  1stcelcls  17187  blsscls2  18050  stdbdbl  18063  xrsblre  18317  icccmplem2  18328  itg1val2  19039  cvxcl  20279  erdszelem8  23140  rescon  23188  cvmliftmolem2  23224  cvmlift2lem12  23256  ax5seglem4  23971  ax5seglem5  23972  axcontlem3  24005  axcontlem8  24010  axcontlem9  24011  broutsideof3  24160  outsideoftr  24163  outsidele  24166  lvsovso3  25040  addcanrg  25079  icccon2  25112  dgrsub2  26751  ltltncvr  28985  atcvrj2b  28994  cvrat4  29005  cvrat42  29006  2at0mat0  29087  islpln2a  29110  paddasslem11  29392  pmod1i  29410  lhpm0atN  29591  lautcvr  29654  cdlemg4c  30174  tendoplass  30345  tendodi1  30346  tendodi2  30347
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