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

Theorem simplr1 999
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 963 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ph )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  soltmin  5232  frfi  7311  wemappo  7474  iccsplit  10985  ccatswrd  11728  sqrmo  12012  pcdvdstr  13204  vdwlem12  13315  mreexexlem4d  13827  iscatd2  13861  oppccomfpropd  13908  resssetc  14202  resscatc  14215  mod1ile  14489  mod2ile  14490  prdsmndd  14683  grprcan  14793  prdsrngd  15673  lmodprop2d  15961  lssintcl  15995  prdslmodd  16000  islmhm2  16069  islbs3  16182  restopnb  17193  regsep2  17394  iuncon  17444  blsscls2  18487  met2ndci  18505  xrsblre  18795  ofldaddlt  24194  erdszelem8  24837  ax5seglem4  25775  ax5seglem5  25776  axcontlem4  25810  axcontlem8  25814  axcontlem9  25815  axcontlem10  25816  btwncomim  25851  btwnswapid  25855  broutsideof3  25964  outsideoftr  25967  outsidele  25970  mendassa  27370  el2wlksotot  28079  cvrletrN  29756  ltltncvr  29905  atcvrj2b  29914  2at0mat0  30007  paddasslem11  30312  pmod1i  30330  lautcvr  30574  tendoplass  31265  tendodi1  31266  tendodi2  31267  cdlemk34  31392
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator