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

Theorem simpll3 998
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 962 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ordiso2  7484  wemappo  7518  iunfictbso  7995  fin1a2lem12  8291  fin1a2lem13  8292  prlem934  8910  ifle  10783  xlesubadd  10842  icoshftf1o  11020  swrdcl  11766  subcn2  12388  rpdvds  13124  qexpz  13270  ramval  13376  0ram  13388  mreexexd  13873  gsumccat  14787  odmulg  15192  pgpfi1  15229  lsmcl  16155  lbsextlem3  16232  coe1mul2  16662  iscnp4  17327  cnpnei  17328  cnconst2  17347  cnpdis  17357  cnhaus  17418  ordthauslem  17447  clscon  17493  nlly2i  17539  txcn  17658  ordthmeolem  17833  flimrest  18015  isfcf  18066  alexsubALTlem4  18081  ghmcnp  18144  utop2nei  18280  blssps  18454  blss  18455  metcnp3  18570  metcnp  18571  xrsxmet  18840  metdseq0  18884  xrhmeo  18971  cfil3i  19222  caucfil  19236  cfilres  19249  fta1b  20092  mumul  20964  lgsfcl2  21086  lgsdir  21114  lgsne0  21117  pjhthmo  22804  xrge0adddir  24215  probun  24677  cnpcon  24917  axbtwnid  25878  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  axcontlem8  25910  outsideofeq  26064  linethru  26087  nacsfix  26766  mzpsubst  26805  diophrw  26817  lzunuz  26826  jm2.19  27064  jm2.27  27079  islindf4  27285  hbtlem5  27309  pmtrf  27374  rfcnnnub  27683  stoweidlem20  27745  stoweidlem61  27786  elfzonelfzo  28132  atlatmstc  30117  cvlcvr1  30137  ishlat3N  30152  hlrelat  30199  intnatN  30204  cvrval5  30212  atcvrlln  30317  llnexatN  30318  2at0mat0  30322  llncvrlpln  30355  lplnexllnN  30361  lplncvrlvol  30413  lncvrelatN  30578  pmapjoin  30649  pmapjat1  30650  pclclN  30688  osumclN  30764  lhprelat3N  30837  cdlemd5  30999  cdleme32fvcl  31237  cdlemg39  31513  ltrncom  31535  dihmeetALTN  32125  dochss  32163  mapdrvallem2  32443
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator