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

Theorem simpll2 1028
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 992 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  wemappo  7784  iunfictbso  8305  fin1a2lem13  8602  prlem934  9223  ifle  11188  ixxlb  11343  elfzonelfzo  11648  swrdcl  12336  subcn2  13093  qexpz  13984  mreexexd  14607  issubmnd  15470  gsumccat  15540  pmtrf  15982  pgpssslw  16134  lsmmod  16193  reslmhm2b  17157  lsmcl  17186  lbsextlem3  17263  coe1mul2  17745  evl1gsumdlem  17812  frlmsslsp  18245  frlmsslspOLD  18246  islindf4  18289  madurid  18472  cramerlem2  18516  iscnp4  18889  cnrest2  18912  ordthauslem  19009  cncmp  19017  clscon  19056  rnelfmlem  19547  flimrest  19578  isfcf  19629  cnpfcf  19636  alexsubALT  19645  cldsubg  19703  utop2nei  19847  neipcfilu  19893  blssps  20021  blss  20022  stdbdbl  20114  metcnp3  20137  nmoeq0  20337  xrsxmet  20408  metdseq0  20452  addcnlem  20462  xrhmeo  20540  nmhmcn  20697  cfilres  20829  lgsfcl2  22663  lgsdir  22691  lgsne0  22694  istrkgcb  22941  axcontlem2  23233  axcontlem7  23238  axcontlem8  23239  pjhthmo  24727  xrge0adddir  26177  probun  26824  trisegint  28081  btwnconn1lem13  28152  outsideoftr  28182  outsideofeq  28183  linethru  28206  mzpsubst  29111  lzunuz  29132  acongeq  29352  jm2.19  29368  jm2.27  29383  aomclem6  29438  lmhmfgsplit  29465  hbtlem5  29510  stoweidlem61  29882  usg2spot2nb  30684  domnmsuppn0  30812  coe1fzgsumdlem  30870  mdetdiaglem  30932  lincresunit3  31012  cnstpmatel2  31065  atlatmstc  33060  cvlcvr1  33080  hlrelat  33142  intnatN  33147  cvrval5  33155  2at0mat0  33265  llncvrlpln  33298  lplnexllnN  33304  lplncvrlvol  33356  lncvrelatN  33521  lncmp  33523  paddasslem5  33564  pmapjoin  33592  pmapjat1  33593  pclclN  33631  lhprelat3N  33780  cdleme32fvcl  34180  cdlemg1a  34310  cdlemg1cN  34327  cdlemg39  34456  ltrncom  34478  dihmeetALTN  35068  dihlspsnat  35074  mapdrvallem2  35386
  Copyright terms: Public domain W3C validator