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

Theorem simpll3 1029
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll3  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 993 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
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:  ordiso2  7721  wemappo  7755  iunfictbso  8276  fin1a2lem12  8572  fin1a2lem13  8573  prlem934  9194  ifle  11159  xlesubadd  11218  icoshftf1o  11400  elfzonelfzo  11619  swrdcl  12307  repswccat  12415  subcn2  13064  rpdvds  13802  qexpz  13955  ramval  14061  0ram  14073  cshwrepswhash1  14121  mreexexd  14578  gsumccat  15510  gsmsymgreqlem1  15926  pmtrf  15952  odmulg  16048  pgpfi1  16085  lsmcl  17141  lbsextlem3  17218  coe1mul2  17698  islindf4  18242  cramerlem2  18469  iscnp4  18842  cnpnei  18843  cnconst2  18862  cnpdis  18872  cnhaus  18933  ordthauslem  18962  clscon  19009  nlly2i  19055  txcn  19174  ordthmeolem  19349  flimrest  19531  isfcf  19582  alexsubALTlem4  19597  ghmcnp  19660  utop2nei  19800  blssps  19974  blss  19975  metcnp3  20090  metcnp  20091  xrsxmet  20361  metdseq0  20405  xrhmeo  20493  cfil3i  20755  caucfil  20769  cfilres  20782  fta1b  21616  mumul  22494  lgsfcl2  22616  lgsdir  22644  lgsne0  22647  istrkgcb  22894  axbtwnid  23136  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  axcontlem8  23168  pjhthmo  24656  xrge0adddir  26106  archiabl  26166  probun  26754  cnpcon  27071  outsideofeq  28112  linethru  28135  nacsfix  29001  mzpsubst  29038  diophrw  29050  lzunuz  29059  jm2.19  29295  jm2.27  29310  hbtlem5  29437  rfcnnnub  29711  stoweidlem20  29768  stoweidlem61  29809  rmsupp0  30732  rmsuppss  30734  fsuppmapnn0fiub0  30750  atlatmstc  32804  cvlcvr1  32824  ishlat3N  32839  hlrelat  32886  intnatN  32891  cvrval5  32899  atcvrlln  33004  llnexatN  33005  2at0mat0  33009  llncvrlpln  33042  lplnexllnN  33048  lplncvrlvol  33100  lncvrelatN  33265  pmapjoin  33336  pmapjat1  33337  pclclN  33375  osumclN  33451  lhprelat3N  33524  cdlemd5  33686  cdleme32fvcl  33924  cdlemg39  34200  ltrncom  34222  dihmeetALTN  34812  dochss  34850  mapdrvallem2  35130
  Copyright terms: Public domain W3C validator