Theorem simp-4l 806

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4l	|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )

Proof of Theorem simp-4l

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

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem is referenced by:  simp-5l  808  marypha1lem  8339  acndom2  8877  ttukeylem6  9336  fpwwe2lem12  9463  reuccats1  13480  dfgcd2  15263  ramcl  15733  initoeu2lem1  16664  gsmsymgreqlem2  17851  dfod2  17981  pgpfi  18020  ghmcyg  18297  psgndif  19948  scmatmulcl  20324  cpmatmcllem  20523  neiptoptop  20935  cncnp  21084  subislly  21284  ptcnplem  21424  pthaus  21441  xkohaus  21456  kqreglem1  21544  cnextcn  21871  qustgplem  21924  trust  22033  utoptop  22038  restutopopn  22042  ustuqtop2  22046  ustuqtop3  22047  utop3cls  22055  utopreg  22056  isucn2  22083  met1stc  22326  metustsym  22360  metuel2  22370  xrge0tsms  22637  xmetdcn2  22640  nmoleub2lem2  22916  iscfil2  23064  iscfil3  23071  dvmptfsum  23738  dvlip2  23758  aannenlem1  24083  ulm2  24139  ulmuni  24146  mtestbdd  24159  efopn  24404  dchrptlem1  24989  pntpbnd  25277  pntibnd  25282  f1otrg  25751  f1otrge  25752  nbupgr  26240  upgriswlk  26537  usgr2pth  26660  clwlkclwwlklem2a4  26898  cusconngr  27051  xrofsup  29533  ressprs  29655  omndmul2  29712  isarchi3  29741  archirngz  29743  lmodslmd  29757  gsummpt2d  29781  xrge0tsmsd  29785  suborng  29815  isarchiofld  29817  sqsscirc1  29954  lmxrge0  29998  lmdvg  29999  esumrnmpt2  30130  esumfsup  30132  esumcvg  30148  esum2d  30155  ddemeas  30299  omssubadd  30362  noetalem3  31865  btwnconn1lem13  32206  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem29  33438  mblfinlem3  33448  mblfinlem4  33449  ftc1anclem7  33491  ftc1anc  33493  prdstotbnd  33593  ltrnid  35421  rencldnfilem  37384  pellex  37399  pellfundex  37450  dvdsacongtr  37551  fnchoice  39188  climsuse  39840  addlimc  39880  0ellimcdiv  39881  limclner  39883  climxrre  39982  xlimmnfvlem2  40059  xlimpnfvlem2  40063  icccncfext  40100  dvnprodlem3  40163  fourierdlem12  40336  fourierdlem34  40358  fourierdlem50  40373  fourierdlem80  40403  fourierdlem81  40404  fourierdlem87  40410  etransclem35  40486  sge0pr  40611  smfmullem3  41000  mogoldbb  41673  uzlidlring  41929  2zlidl  41934