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

Theorem simpll3 1038
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 1002 . 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 974
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 976
This theorem is referenced by:  ordiso2  7943  wemappo  7977  iunfictbso  8498  fin1a2lem12  8794  fin1a2lem13  8795  prlem934  9414  ifle  11406  xlesubadd  11465  icoshftf1o  11653  elfzonelfzo  11893  fsuppmapnn0fiub0  12080  swrdcl  12627  repswccat  12738  subcn2  13398  rpdvds  14246  qexpz  14401  ramval  14507  0ram  14519  cshwrepswhash1  14568  mreexexd  15026  gsumccat  15987  gsmsymgreqlem1  16433  pmtrf  16458  odmulg  16556  pgpfi1  16593  lsmcl  17707  lbsextlem3  17784  coe1mul2  18288  islindf4  18850  cramerlem2  19167  cpmadugsumlemF  19354  cayhamlem4  19366  iscnp4  19741  cnpnei  19742  cnconst2  19761  cnpdis  19771  cnhaus  19832  ordthauslem  19861  clscon  19908  nlly2i  19954  txcn  20104  ordthmeolem  20279  flimrest  20461  isfcf  20512  alexsubALTlem4  20527  ghmcnp  20590  utop2nei  20730  blssps  20904  blss  20905  metcnp3  21020  metcnp  21021  xrsxmet  21291  metdseq0  21335  xrhmeo  21423  cfil3i  21685  caucfil  21699  cfilres  21712  fta1b  22547  mumul  23431  lgsfcl2  23553  lgsdir  23581  lgsne0  23584  istrkgcb  23829  axbtwnid  24218  axcontlem2  24244  axcontlem4  24246  axcontlem7  24249  axcontlem8  24250  pjhthmo  26196  xrge0adddir  27659  archiabl  27719  pcmplfinf  27841  probun  28335  cnpcon  28652  outsideofeq  29755  linethru  29778  nacsfix  30619  mzpsubst  30656  diophrw  30667  lzunuz  30676  jm2.19  30910  jm2.27  30925  hbtlem5  31052  rfcnnnub  31365  3adantll2  31374  iccintsng  31499  mullimc  31530  mullimcf  31537  limcperiod  31542  cncfshift  31583  cncfperiod  31588  icccncfext  31597  stoweidlem20  31691  stoweidlem61  31732  fourierdlem73  31851  rmsupp0  32696  rmsuppss  32698  atlatmstc  34784  cvlcvr1  34804  ishlat3N  34819  hlrelat  34866  intnatN  34871  cvrval5  34879  atcvrlln  34984  llnexatN  34985  2at0mat0  34989  llncvrlpln  35022  lplnexllnN  35028  lplncvrlvol  35080  lncvrelatN  35245  pmapjoin  35316  pmapjat1  35317  pclclN  35355  osumclN  35431  lhprelat3N  35504  cdlemd5  35667  cdleme32fvcl  35906  cdlemg39  36182  ltrncom  36204  dihmeetALTN  36794  dochss  36832  mapdrvallem2  37112
  Copyright terms: Public domain W3C validator