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

Theorem simpll3 996
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 960 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ordiso2  7246  wemappo  7280  iunfictbso  7757  fin1a2lem12  8053  fin1a2lem13  8054  prlem934  8673  ifle  10540  xlesubadd  10599  icoshftf1o  10775  swrdcl  11468  subcn2  12084  rpdvds  12819  qexpz  12965  ramval  13071  0ram  13083  mreexexd  13566  gsumccat  14480  odmulg  14885  pgpfi1  14922  lsmcl  15852  lbsextlem3  15929  coe1mul2  16362  cnpnei  17009  cnconst2  17027  cnpdis  17037  cnhaus  17098  ordthauslem  17127  clscon  17172  nlly2i  17218  txcn  17336  ordthmeolem  17508  flimrest  17694  isfcf  17745  alexsubALTlem4  17760  ghmcnp  17813  blss  17988  metcnp3  18102  metcnp  18103  xrsxmet  18331  metdseq0  18374  xrhmeo  18460  cfil3i  18711  caucfil  18725  cfilres  18738  fta1b  19571  mumul  20435  lgsfcl2  20557  lgsdir  20585  lgsne0  20588  pjhthmo  21897  xrge0adddir  23347  probun  23637  cnpcon  23776  axbtwnid  24639  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  outsideofeq  24825  linethru  24848  iscnp4  25666  limptlimpr2lem2  25678  nacsfix  26890  mzpsubst  26929  diophrw  26941  lzunuz  26950  jm2.19  27189  jm2.27  27204  islindf4  27411  hbtlem5  27435  pmtrf  27500  rfcnnnub  27810  stoweidlem20  27872  stoweidlem61  27913  atlatmstc  30131  cvlcvr1  30151  ishlat3N  30166  hlrelat  30213  intnatN  30218  cvrval5  30226  atcvrlln  30331  llnexatN  30332  2at0mat0  30336  llncvrlpln  30369  lplnexllnN  30375  lplncvrlvol  30427  lncvrelatN  30592  pmapjoin  30663  pmapjat1  30664  pclclN  30702  osumclN  30778  lhprelat3N  30851  cdlemd5  31013  cdleme32fvcl  31251  cdlemg39  31527  ltrncom  31549  dihmeetALTN  32139  dochss  32177  mapdrvallem2  32457
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