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

Theorem simpll2 1048
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 1012 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  f1prex  6182  wemappo  8064  iunfictbso  8545  fin1a2lem13  8842  prlem934  9458  ifle  11490  ixxlb  11657  ixxlbOLD  11658  elfzonelfzo  12011  swrdcl  12775  subcn2  13658  qexpz  14846  mreexexd  15554  initoeu2lem2  15910  issubmnd  16564  gsumccat  16625  frmdup3lem  16650  pmtrf  17096  pgpssslw  17266  lsmmod  17325  reslmhm2b  18277  lsmcl  18306  lbsextlem3  18383  coe1mul2  18862  coe1fzgsumdlem  18895  evl1gsumdlem  18944  frlmsslsp  19354  islindf4  19396  scmate  19535  mdetdiaglem  19623  madurid  19669  cramerlem2  19713  pmatcollpw3lem  19807  iscnp4  20279  cnrest2  20302  ordthauslem  20399  cncmp  20407  clscon  20445  rnelfmlem  20967  flimrest  20998  isfcf  21049  cnpfcf  21056  alexsubALT  21066  cldsubg  21125  utop2nei  21265  neipcfilu  21311  blssps  21439  blss  21440  stdbdbl  21532  metcnp3  21555  nmoeq0  21757  xrsxmet  21827  metdseq0  21871  metdseq0OLD  21886  addcnlem  21896  xrhmeo  21974  nmhmcn  22134  cfilres  22266  lgsfcl2  24230  lgsdir  24258  lgsne0  24261  istrkgcb  24504  axcontlem2  24995  axcontlem7  25000  axcontlem8  25001  usg2spot2nb  25793  pjhthmo  26955  xrge0adddir  28455  pcmplfinf  28688  probun  29252  trisegint  30795  btwnconn1lem13  30866  outsideoftr  30896  outsideofeq  30897  linethru  30920  isbasisrelowllem1  31758  atlatmstc  32885  cvlcvr1  32905  hlrelat  32967  intnatN  32972  cvrval5  32980  2at0mat0  33090  llncvrlpln  33123  lplnexllnN  33129  lplncvrlvol  33181  lncvrelatN  33346  lncmp  33348  paddasslem5  33389  pmapjoin  33417  pmapjat1  33418  pclclN  33456  lhprelat3N  33605  cdleme32fvcl  34007  cdlemg1a  34137  cdlemg1cN  34154  cdlemg39  34283  ltrncom  34305  dihmeetALTN  34895  dihlspsnat  34901  mapdrvallem2  35213  mzpsubst  35590  lzunuz  35610  acongeq  35833  jm2.19  35848  jm2.27  35863  aomclem6  35917  lmhmfgsplit  35944  hbtlem5  35987  iunrelexpuztr  36311  3adantll3  37365  ioondisj2  37589  ioondisj1  37590  iccintsng  37624  icccncfext  37765  stoweidlem61  37922  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem73  38043  subupgr  39359  domnmsuppn0  40207  lincresunit3  40327  nnolog2flm1  40454
  Copyright terms: Public domain W3C validator