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  5082  frfi  7102  wemappo  7264  iccsplit  10768  ccatswrd  11459  sqrmo  11737  pcdvdstr  12928  vdwlem12  13039  mreexexlem4d  13549  iscatd2  13583  oppccomfpropd  13630  resssetc  13924  resscatc  13937  mod1ile  14211  mod2ile  14212  prdsmndd  14405  grprcan  14515  prdsrngd  15395  lmodprop2d  15687  lssintcl  15721  prdslmodd  15726  islmhm2  15795  islbs3  15908  restopnb  16906  regsep2  17104  iuncon  17154  blsscls2  18050  met2ndci  18068  xrsblre  18317  erdszelem8  23729  ax5seglem4  24560  ax5seglem5  24561  axcontlem4  24595  axcontlem8  24599  axcontlem9  24600  axcontlem10  24601  btwncomim  24636  btwnswapid  24640  broutsideof3  24749  outsideoftr  24752  outsidele  24755  addcanrg  25667  mendassa  27502  cvrletrN  29463  ltltncvr  29612  atcvrj2b  29621  2at0mat0  29714  paddasslem11  30019  pmod1i  30037  lautcvr  30281  tendoplass  30972  tendodi1  30973  tendodi2  30974  cdlemk34  31099
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