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

Theorem simpll3 1046
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 1010 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 466 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  f1prex  6193  ordiso2  8032  wemappo  8066  iunfictbso  8545  fin1a2lem12  8841  fin1a2lem13  8842  prlem934  9458  ifle  11490  xlesubadd  11549  icoshftf1o  11755  elfzonelfzo  12010  fsuppmapnn0fiub0  12204  swrdcl  12765  repswccat  12878  subcn2  13645  rpdvds  14663  coprmprod  14665  qexpz  14833  ramval  14947  ramvalOLD  14948  0ram  14965  cshwrepswhash1  15060  mreexexd  15541  gsumccat  16612  gsmsymgreqlem1  17058  pmtrf  17083  odmulg  17194  pgpfi1  17234  lsmcl  18293  lbsextlem3  18370  coe1mul2  18849  islindf4  19382  cramerlem2  19699  cpmadugsumlemF  19886  cayhamlem4  19898  iscnp4  20265  cnpnei  20266  cnconst2  20285  cnpdis  20295  cnhaus  20356  ordthauslem  20385  clscon  20431  nlly2i  20477  txcn  20627  ordthmeolem  20802  flimrest  20984  isfcf  21035  alexsubALTlem4  21051  ghmcnp  21115  utop2nei  21251  blssps  21425  blss  21426  metcnp3  21541  metcnp  21542  xrsxmet  21813  metdseq0  21857  metdseq0OLD  21872  xrhmeo  21960  cfil3i  22225  caucfil  22239  cfilres  22252  fta1b  23106  mumul  24094  lgsfcl2  24216  lgsdir  24244  lgsne0  24247  istrkgcb  24490  axbtwnid  24955  axcontlem2  24981  axcontlem4  24983  axcontlem7  24986  axcontlem8  24987  pjhthmo  26940  xrge0adddir  28449  archiabl  28509  pcmplfinf  28683  probun  29247  cnpcon  29948  outsideofeq  30889  linethru  30912  atlatmstc  32803  cvlcvr1  32823  ishlat3N  32838  hlrelat  32885  intnatN  32890  cvrval5  32898  atcvrlln  33003  llnexatN  33004  2at0mat0  33008  llncvrlpln  33041  lplnexllnN  33047  lplncvrlvol  33099  lncvrelatN  33264  pmapjoin  33335  pmapjat1  33336  pclclN  33374  osumclN  33450  lhprelat3N  33523  cdlemd5  33686  cdleme32fvcl  33925  cdlemg39  34201  ltrncom  34223  dihmeetALTN  34813  dochss  34851  mapdrvallem2  35131  nacsfix  35472  mzpsubst  35508  diophrw  35519  lzunuz  35528  jm2.19  35767  jm2.27  35782  hbtlem5  35906  iunrelexpuztr  36170  rfcnnnub  37217  3adantll2  37224  iccintsng  37454  mullimc  37515  mullimcf  37522  limcperiod  37527  cncfshift  37570  cncfperiod  37575  icccncfext  37584  stoweidlem20  37699  stoweidlem61  37741  fourierdlem73  37862  rmsupp0  39426  rmsuppss  39428
  Copyright terms: Public domain W3C validator