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  7264  iunfictbso  7741  fin1a2lem13  8038  prlem934  8657  ifle  10524  ixxlb  10678  swrdcl  11452  subcn2  12068  qexpz  12949  mreexexd  13550  issubmnd  14401  gsumccat  14464  pgpssslw  14925  lsmmod  14984  reslmhm2b  15811  lsmcl  15836  lbsextlem3  15913  coe1mul2  16346  cnrest2  17014  ordthauslem  17111  cncmp  17119  clscon  17156  rnelfmlem  17647  flimrest  17678  isfcf  17729  cnpfcf  17736  alexsubALT  17745  cldsubg  17793  blss  17972  stdbdbl  18063  metcnp3  18086  nmoeq0  18245  xrsxmet  18315  metdseq0  18358  addcnlem  18368  xrhmeo  18444  nmhmcn  18601  cfilres  18722  lgsfcl2  20541  lgsdir  20569  lgsne0  20572  pjhthmo  21881  xrge0adddir  23332  probun  23622  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  trisegint  24651  btwnconn1lem13  24722  outsideoftr  24752  outsideofeq  24753  linethru  24776  iscnp4  25563  icccon2  25700  mzpsubst  26826  lzunuz  26847  acongeq  27070  jm2.19  27086  jm2.27  27101  aomclem6  27156  lmhmfgsplit  27184  uvcresum  27242  frlmsslsp  27248  islindf4  27308  hbtlem5  27332  pmtrf  27397  stoweidlem61  27810  atlatmstc  29509  cvlcvr1  29529  hlrelat  29591  intnatN  29596  cvrval5  29604  2at0mat0  29714  llncvrlpln  29747  lplnexllnN  29753  lplncvrlvol  29805  lncvrelatN  29970  lncmp  29972  paddasslem5  30013  pmapjoin  30041  pmapjat1  30042  pclclN  30080  lhprelat3N  30229  cdleme32fvcl  30629  cdlemg1a  30759  cdlemg1cN  30776  cdlemg39  30905  ltrncom  30927  dihmeetALTN  31517  dihlspsnat  31523  mapdrvallem2  31835
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