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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 961 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  wemappo  7518  iunfictbso  7995  fin1a2lem13  8292  prlem934  8910  ifle  10783  ixxlb  10938  swrdcl  11766  subcn2  12388  qexpz  13270  mreexexd  13873  issubmnd  14724  gsumccat  14787  pgpssslw  15248  lsmmod  15307  reslmhm2b  16130  lsmcl  16155  lbsextlem3  16232  coe1mul2  16662  iscnp4  17327  cnrest2  17350  ordthauslem  17447  cncmp  17455  clscon  17493  rnelfmlem  17984  flimrest  18015  isfcf  18066  cnpfcf  18073  alexsubALT  18082  cldsubg  18140  utop2nei  18280  neipcfilu  18326  blssps  18454  blss  18455  stdbdbl  18547  metcnp3  18570  nmoeq0  18770  xrsxmet  18840  metdseq0  18884  addcnlem  18894  xrhmeo  18971  nmhmcn  19128  cfilres  19249  lgsfcl2  21086  lgsdir  21114  lgsne0  21117  pjhthmo  22804  xrge0adddir  24215  probun  24677  axcontlem2  25904  axcontlem7  25909  axcontlem8  25910  trisegint  25962  btwnconn1lem13  26033  outsideoftr  26063  outsideofeq  26064  linethru  26087  mzpsubst  26805  lzunuz  26826  acongeq  27048  jm2.19  27064  jm2.27  27079  aomclem6  27134  lmhmfgsplit  27161  uvcresum  27219  frlmsslsp  27225  islindf4  27285  hbtlem5  27309  pmtrf  27374  stoweidlem61  27786  elfzonelfzo  28132  usg2spot2nb  28454  atlatmstc  30117  cvlcvr1  30137  hlrelat  30199  intnatN  30204  cvrval5  30212  2at0mat0  30322  llncvrlpln  30355  lplnexllnN  30361  lplncvrlvol  30413  lncvrelatN  30578  lncmp  30580  paddasslem5  30621  pmapjoin  30649  pmapjat1  30650  pclclN  30688  lhprelat3N  30837  cdleme32fvcl  31237  cdlemg1a  31367  cdlemg1cN  31384  cdlemg39  31513  ltrncom  31535  dihmeetALTN  32125  dihlspsnat  32131  mapdrvallem2  32443
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