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

Theorem simpll2 995
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 959 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  wemappo  7280  iunfictbso  7757  fin1a2lem13  8054  prlem934  8673  ifle  10540  ixxlb  10694  swrdcl  11468  subcn2  12084  qexpz  12965  mreexexd  13566  issubmnd  14417  gsumccat  14480  pgpssslw  14941  lsmmod  15000  reslmhm2b  15827  lsmcl  15852  lbsextlem3  15929  coe1mul2  16362  cnrest2  17030  ordthauslem  17127  cncmp  17135  clscon  17172  rnelfmlem  17663  flimrest  17694  isfcf  17745  cnpfcf  17752  alexsubALT  17761  cldsubg  17809  blss  17988  stdbdbl  18079  metcnp3  18102  nmoeq0  18261  xrsxmet  18331  metdseq0  18374  addcnlem  18384  xrhmeo  18460  nmhmcn  18617  cfilres  18738  lgsfcl2  20557  lgsdir  20585  lgsne0  20588  pjhthmo  21897  xrge0adddir  23347  probun  23637  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  trisegint  24723  btwnconn1lem13  24794  outsideoftr  24824  outsideofeq  24825  linethru  24848  iscnp4  25666  icccon2  25803  mzpsubst  26929  lzunuz  26950  acongeq  27173  jm2.19  27189  jm2.27  27204  aomclem6  27259  lmhmfgsplit  27287  uvcresum  27345  frlmsslsp  27351  islindf4  27411  hbtlem5  27435  pmtrf  27500  stoweidlem61  27913  atlatmstc  30131  cvlcvr1  30151  hlrelat  30213  intnatN  30218  cvrval5  30226  2at0mat0  30336  llncvrlpln  30369  lplnexllnN  30375  lplncvrlvol  30427  lncvrelatN  30592  lncmp  30594  paddasslem5  30635  pmapjoin  30663  pmapjat1  30664  pclclN  30702  lhprelat3N  30851  cdleme32fvcl  31251  cdlemg1a  31381  cdlemg1cN  31398  cdlemg39  31527  ltrncom  31549  dihmeetALTN  32139  dihlspsnat  32145  mapdrvallem2  32457
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