Theorem simpll3 1102

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll3	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1066	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 481	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1prex  6539  ordiso2  8420  wemappo  8454  iunfictbso  8937  fin1a2lem12  9233  fin1a2lem13  9234  prlem934  9855  ifle  12028  xlesubadd  12093  icoshftf1o  12295  elfzonelfzo  12570  fsuppmapnn0fiub0  12793  swrdcl  13419  repswccat  13532  subcn2  14325  rpdvds  15374  coprmprod  15375  qexpz  15605  ramval  15712  0ram  15724  cshwrepswhash1  15809  mreexexd  16308  mreexexdOLD  16309  gsumccat  17378  gsmsymgreqlem1  17850  pmtrf  17875  odmulg  17973  pgpfi1  18010  lsmcl  19083  lbsextlem3  19160  coe1mul2  19639  islindf4  20177  cramerlem2  20494  cpmadugsumlemF  20681  cayhamlem4  20693  iscnp4  21067  cnpnei  21068  cnconst2  21087  cnpdis  21097  cnhaus  21158  ordthauslem  21187  clsconn  21233  nlly2i  21279  txcn  21429  ordthmeolem  21604  flimrest  21787  isfcf  21838  alexsubALTlem4  21854  ghmcnp  21918  utop2nei  22054  blssps  22229  blss  22230  metcnp3  22345  metcnp  22346  xrsxmet  22612  metdseq0  22657  xrhmeo  22745  cfil3i  23067  caucfil  23081  cfilres  23094  fta1b  23929  mumul  24907  lgsfcl2  25028  lgsdir  25057  lgsne0  25060  istrkgcb  25355  axbtwnid  25819  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  umgr2v2enb1  26422  wpthswwlks2on  26854  frgr3v  27139  numclwlk1lem2foa  27224  pjhthmo  28161  xrge0adddir  29692  archiabl  29752  pcmplfinf  29928  probun  30481  cnpconn  31212  nolt02o  31845  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd2  31862  outsideofeq  32237  linethru  32260  atlatmstc  34606  cvlcvr1  34626  ishlat3N  34641  hlrelat  34688  intnatN  34693  cvrval5  34701  atcvrlln  34806  llnexatN  34807  2at0mat0  34811  llncvrlpln  34844  lplnexllnN  34850  lplncvrlvol  34902  lncvrelatN  35067  pmapjoin  35138  pmapjat1  35139  pclclN  35177  osumclN  35253  lhprelat3N  35326  cdlemd5  35489  cdleme32fvcl  35728  cdlemg39  36004  ltrncom  36026  dihmeetALTN  36616  dochss  36654  mapdrvallem2  36934  nacsfix  37275  mzpsubst  37311  diophrw  37322  lzunuz  37331  jm2.19  37560  jm2.27  37575  hbtlem5  37698  iunrelexpuztr  38011  rfcnnnub  39195  3adantll2  39202  infleinf  39588  iccintsng  39749  mullimc  39848  mullimcf  39855  limcperiod  39860  cncfshift  40087  cncfperiod  40092  icccncfext  40100  stoweidlem20  40237  stoweidlem61  40278  fourierdlem73  40396  rmsupp0  42149  rmsuppss  42151