MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplr1 Structured version   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  5273  frfi  7352  wemappo  7518  iccsplit  11029  ccatswrd  11773  sqrmo  12057  pcdvdstr  13249  vdwlem12  13360  mreexexlem4d  13872  iscatd2  13906  oppccomfpropd  13953  resssetc  14247  resscatc  14260  mod1ile  14534  mod2ile  14535  prdsmndd  14728  grprcan  14838  prdsrngd  15718  lmodprop2d  16006  lssintcl  16040  prdslmodd  16045  islmhm2  16114  islbs3  16227  restopnb  17239  regsep2  17440  iuncon  17491  blsscls2  18534  met2ndci  18552  xrsblre  18842  ofldaddlt  24241  erdszelem8  24884  ax5seglem4  25871  ax5seglem5  25872  axcontlem4  25906  axcontlem8  25910  axcontlem9  25911  axcontlem10  25912  btwncomim  25947  btwnswapid  25951  broutsideof3  26060  outsideoftr  26063  outsidele  26066  mendassa  27479  subsubelfzo0  28135  el2wlksotot  28349  cvrletrN  30071  ltltncvr  30220  atcvrj2b  30229  2at0mat0  30322  paddasslem11  30627  pmod1i  30645  lautcvr  30889  tendoplass  31580  tendodi1  31581  tendodi2  31582  cdlemk34  31707
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