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

Theorem simpll2 1034
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 998 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 463 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  f1prex  6106  wemappo  7907  iunfictbso  8426  fin1a2lem13  8723  prlem934  9340  ifle  11335  ixxlb  11490  elfzonelfzo  11830  swrdcl  12574  subcn2  13438  qexpz  14441  mreexexd  15074  initoeu2lem2  15430  issubmnd  16084  gsumccat  16145  frmdup3lem  16170  pmtrf  16616  pgpssslw  16770  lsmmod  16829  reslmhm2b  17832  lsmcl  17861  lbsextlem3  17938  coe1mul2  18442  coe1fzgsumdlem  18475  evl1gsumdlem  18524  frlmsslsp  18935  islindf4  18977  scmate  19116  mdetdiaglem  19204  madurid  19250  cramerlem2  19294  pmatcollpw3lem  19388  iscnp4  19869  cnrest2  19892  ordthauslem  19989  cncmp  19997  clscon  20035  rnelfmlem  20557  flimrest  20588  isfcf  20639  cnpfcf  20646  alexsubALT  20655  cldsubg  20713  utop2nei  20857  neipcfilu  20903  blssps  21031  blss  21032  stdbdbl  21124  metcnp3  21147  nmoeq0  21347  xrsxmet  21418  metdseq0  21462  addcnlem  21472  xrhmeo  21550  nmhmcn  21707  cfilres  21839  lgsfcl2  23713  lgsdir  23741  lgsne0  23744  istrkgcb  23989  axcontlem2  24410  axcontlem7  24415  axcontlem8  24416  usg2spot2nb  25207  pjhthmo  26358  xrge0adddir  27865  pcmplfinf  28049  probun  28577  trisegint  29867  btwnconn1lem13  29938  outsideoftr  29968  outsideofeq  29969  linethru  29992  mzpsubst  30882  lzunuz  30902  acongeq  31122  jm2.19  31137  jm2.27  31152  aomclem6  31207  lmhmfgsplit  31234  hbtlem5  31281  3adantll3  31624  ioondisj2  31726  ioondisj1  31727  iccintsng  31764  icccncfext  31891  stoweidlem61  32044  fourierdlem42  32132  fourierdlem73  32163  domnmsuppn0  33197  lincresunit3  33317  nnolog2flm1  33446  atlatmstc  35492  cvlcvr1  35512  hlrelat  35574  intnatN  35579  cvrval5  35587  2at0mat0  35697  llncvrlpln  35730  lplnexllnN  35736  lplncvrlvol  35788  lncvrelatN  35953  lncmp  35955  paddasslem5  35996  pmapjoin  36024  pmapjat1  36025  pclclN  36063  lhprelat3N  36212  cdleme32fvcl  36614  cdlemg1a  36744  cdlemg1cN  36761  cdlemg39  36890  ltrncom  36912  dihmeetALTN  37502  dihlspsnat  37508  mapdrvallem2  37820  iunrelexpuztr  38259
  Copyright terms: Public domain W3C validator