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

Theorem simpll3 1035
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 999 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 463 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
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:  ordiso2  7932  wemappo  7966  iunfictbso  8486  fin1a2lem12  8782  fin1a2lem13  8783  prlem934  9400  ifle  11399  xlesubadd  11458  icoshftf1o  11646  elfzonelfzo  11893  fsuppmapnn0fiub0  12084  swrdcl  12638  repswccat  12751  subcn2  13502  rpdvds  14352  qexpz  14507  ramval  14613  0ram  14625  cshwrepswhash1  14674  mreexexd  15140  gsumccat  16211  gsmsymgreqlem1  16657  pmtrf  16682  odmulg  16780  pgpfi1  16817  lsmcl  17927  lbsextlem3  18004  coe1mul2  18508  islindf4  19043  cramerlem2  19360  cpmadugsumlemF  19547  cayhamlem4  19559  iscnp4  19934  cnpnei  19935  cnconst2  19954  cnpdis  19964  cnhaus  20025  ordthauslem  20054  clscon  20100  nlly2i  20146  txcn  20296  ordthmeolem  20471  flimrest  20653  isfcf  20704  alexsubALTlem4  20719  ghmcnp  20782  utop2nei  20922  blssps  21096  blss  21097  metcnp3  21212  metcnp  21213  xrsxmet  21483  metdseq0  21527  xrhmeo  21615  cfil3i  21877  caucfil  21891  cfilres  21904  fta1b  22739  mumul  23656  lgsfcl2  23778  lgsdir  23806  lgsne0  23809  istrkgcb  24054  axbtwnid  24447  axcontlem2  24473  axcontlem4  24475  axcontlem7  24478  axcontlem8  24479  pjhthmo  26421  xrge0adddir  27919  archiabl  27979  pcmplfinf  28102  probun  28625  cnpcon  28942  outsideofeq  30011  linethru  30034  nacsfix  30887  mzpsubst  30923  diophrw  30934  lzunuz  30943  jm2.19  31177  jm2.27  31192  hbtlem5  31321  rfcnnnub  31654  3adantll2  31663  iccintsng  31805  mullimc  31864  mullimcf  31871  limcperiod  31876  cncfshift  31918  cncfperiod  31923  icccncfext  31932  stoweidlem20  32044  stoweidlem61  32085  fourierdlem73  32204  rmsupp0  33234  rmsuppss  33236  atlatmstc  35460  cvlcvr1  35480  ishlat3N  35495  hlrelat  35542  intnatN  35547  cvrval5  35555  atcvrlln  35660  llnexatN  35661  2at0mat0  35665  llncvrlpln  35698  lplnexllnN  35704  lplncvrlvol  35756  lncvrelatN  35921  pmapjoin  35992  pmapjat1  35993  pclclN  36031  osumclN  36107  lhprelat3N  36180  cdlemd5  36343  cdleme32fvcl  36582  cdlemg39  36858  ltrncom  36880  dihmeetALTN  37470  dochss  37508  mapdrvallem2  37788  iunrelexpuztr  38227
  Copyright terms: Public domain W3C validator