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  7230  wemappo  7264  iunfictbso  7741  fin1a2lem12  8037  fin1a2lem13  8038  prlem934  8657  ifle  10524  xlesubadd  10583  icoshftf1o  10759  swrdcl  11452  subcn2  12068  rpdvds  12803  qexpz  12949  ramval  13055  0ram  13067  mreexexd  13550  gsumccat  14464  odmulg  14869  pgpfi1  14906  lsmcl  15836  lbsextlem3  15913  coe1mul2  16346  cnpnei  16993  cnconst2  17011  cnpdis  17021  cnhaus  17082  ordthauslem  17111  clscon  17156  nlly2i  17202  txcn  17320  ordthmeolem  17492  flimrest  17678  isfcf  17729  alexsubALTlem4  17744  ghmcnp  17797  blss  17972  metcnp3  18086  metcnp  18087  xrsxmet  18315  metdseq0  18358  xrhmeo  18444  cfil3i  18695  caucfil  18709  cfilres  18722  fta1b  19555  mumul  20419  lgsfcl2  20541  lgsdir  20569  lgsne0  20572  pjhthmo  21881  xrge0adddir  23332  probun  23622  cnpcon  23761  axbtwnid  24567  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  outsideofeq  24753  linethru  24776  iscnp4  25563  limptlimpr2lem2  25575  nacsfix  26787  mzpsubst  26826  diophrw  26838  lzunuz  26847  jm2.19  27086  jm2.27  27101  islindf4  27308  hbtlem5  27332  pmtrf  27397  rfcnnnub  27707  stoweidlem20  27769  stoweidlem61  27810  atlatmstc  29509  cvlcvr1  29529  ishlat3N  29544  hlrelat  29591  intnatN  29596  cvrval5  29604  atcvrlln  29709  llnexatN  29710  2at0mat0  29714  llncvrlpln  29747  lplnexllnN  29753  lplncvrlvol  29805  lncvrelatN  29970  pmapjoin  30041  pmapjat1  30042  pclclN  30080  osumclN  30156  lhprelat3N  30229  cdlemd5  30391  cdleme32fvcl  30629  cdlemg39  30905  ltrncom  30927  dihmeetALTN  31517  dochss  31555  mapdrvallem2  31835
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