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

Theorem simplr1 997
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ph )

Proof of Theorem simplr1
StepHypRef Expression
1 simpr1 961 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ph )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ph )
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  sqrmo  11753  pcdvdstr  12944  vdwlem12  13055  mreexexlem4d  13565  iscatd2  13599  oppccomfpropd  13646  resssetc  13940  resscatc  13953  mod1ile  14227  mod2ile  14228  prdsmndd  14421  grprcan  14531  prdsrngd  15411  lmodprop2d  15703  lssintcl  15737  prdslmodd  15742  islmhm2  15811  islbs3  15924  restopnb  16922  regsep2  17120  iuncon  17170  blsscls2  18066  met2ndci  18084  xrsblre  18333  erdszelem8  23744  ax5seglem4  24632  ax5seglem5  24633  axcontlem4  24667  axcontlem8  24671  axcontlem9  24672  axcontlem10  24673  btwncomim  24708  btwnswapid  24712  broutsideof3  24821  outsideoftr  24824  outsidele  24827  addcanrg  25770  mendassa  27605  cvrletrN  30085  ltltncvr  30234  atcvrj2b  30243  2at0mat0  30336  paddasslem11  30641  pmod1i  30659  lautcvr  30903  tendoplass  31594  tendodi1  31595  tendodi2  31596  cdlemk34  31721
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