Theorem simp1l 1085

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

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

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

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:  simpl1l  1112  simpr1l  1118  simp11l  1172  simp21l  1178  simp31l  1184  funprgOLD  5941  tfisi  7058  omeulem2  7663  uniinqs  7827  unxpdomlem3  8166  elfiun  8336  cantnffval  8560  tcrank  8747  cofsmo  9091  isfin2-2  9141  tskint  9607  tskun  9608  tskurn  9611  gruina  9640  dedekind  10200  dmdcan  10735  lt2msq1  10907  supmullem1  10993  supmul  10995  xaddass  12079  xaddass2  12080  xlt2add  12090  xmulasslem3  12116  xadddi2r  12128  iccsplit  12305  expaddzlem  12903  expaddz  12904  expmulz  12906  ccatopth2  13471  swrdccat3  13492  resqrtcl  13994  limsupgle  14208  o1add  14344  o1mul  14345  o1sub  14346  bitsfzo  15157  sadfval  15174  smufval  15199  prmexpb  15430  4sqlem18  15666  vdwlem10  15694  fsets  15891  setsstruct2  15896  submre  16265  mrelatlub  17186  mndodcong  17961  subgabl  18241  gex2abl  18254  cntzsubr  18812  abvres  18839  lbsind2  19081  lspsneu  19123  lbsextlem2  19159  lbsextg  19162  lindfind2  20157  matring  20249  maducoeval  20445  maducoeval2  20446  maduf  20447  madurid  20450  gsummatr01  20465  cramerimplem3  20491  cnprest  21093  hausnei2  21157  isreg2  21181  cmpcld  21205  llyrest  21288  nllyrest  21289  csdfil  21698  hausflimlem  21783  ssblps  22227  ssbl  22228  cphassi  23014  cphassir  23015  4cphipval2  23041  cphipval  23042  dvres2  23676  plyadd  23973  plymul  23974  coeeu  23981  vieta1  24067  aalioulem3  24089  aalioulem4  24090  efgh  24287  cxpadd  24425  cxpsub  24428  mulcxp  24431  divcxp  24433  cxple2  24443  cxplt2  24444  cxpcn3lem  24488  angcan  24532  ang180lem5  24543  isosctrlem3  24550  logexprlim  24950  lgssq  25062  abvcxp  25304  padicabv  25319  brbtwn2  25785  ax5seglem6  25814  axcontlem4  25847  axcontlem8  25851  uhgr2edg  26100  nbgrisvtx  26255  nbupgrres  26266  frgrreggt1  27251  chscllem4  28499  ogrpinvlt  29724  eqfunresadj  31659  poseq  31750  wsuclemOLD  31774  nosupbnd2lem1  31861  noetalem5  31867  ifscgr  32151  matunitlindflem1  33405  lshpnelb  34271  lfl1  34357  lshpkrlem6  34402  lshpkrex  34405  hlrelat3  34698  atbtwnexOLDN  34733  atbtwnex  34734  3dim3  34755  3atlem5  34773  2llnmat  34810  lvolex3N  34824  lvolnle3at  34868  4atlem11  34895  4atlem12  34898  dalemccea  34969  cdlema2N  35078  paddasslem2  35107  atmod1i1m  35144  lhp2lt  35287  lhp0lt  35289  lhpj1  35308  lhpmcvr4N  35312  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  cdlemb2  35327  lhple  35328  lhpat  35329  4atex  35362  4atex2-0aOLDN  35364  4atex3  35367  ldilco  35402  ltrncl  35411  ltrn11  35412  ltrnle  35415  ltrncnvleN  35416  ltrnm  35417  ltrnj  35418  ltrncvr  35419  ltrnatb  35423  ltrnel  35425  ltrncnvel  35428  ltrncnv  35432  ltrnmwOLD  35438  trlval2  35450  trlcnv  35452  trljat1  35453  trljat2  35454  trl0  35457  ltrnnidn  35461  trlnidatb  35464  cdlemc1  35478  cdlemc2  35479  cdlemc5  35482  cdlemc6  35483  cdlemd3  35487  cdlemd6  35490  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0e  35504  cdleme0fN  35505  cdleme01N  35508  cdleme02N  35509  cdleme0ex1N  35510  cdleme0moN  35512  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme16aN  35546  cdleme11a  35547  cdleme11fN  35551  cdleme11g  35552  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme12  35558  cdleme13  35559  cdleme17c  35575  cdleme17d1  35576  cdleme18a  35578  cdleme18b  35579  cdleme18c  35580  cdleme22gb  35581  cdlemeda  35585  cdlemednpq  35586  cdlemednuN  35587  cdleme19c  35593  cdleme20aN  35597  cdleme20bN  35598  cdleme20c  35599  cdleme22aa  35627  cdleme22a  35628  cdleme22b  35629  cdleme22d  35631  cdleme22e  35632  cdleme27cl  35654  cdleme27a  35655  cdleme30a  35666  cdleme42a  35759  cdleme42c  35760  cdleme50laut  35835  cdlemf1  35849  cdlemf  35851  cdlemfnid  35852  trlord  35857  cdlemg2fv2  35888  cdlemg2kq  35890  cdlemg2m  35892  cdlemg4a  35896  cdlemg4d  35901  cdlemg4g  35904  cdlemg4  35905  cdlemg6c  35908  cdlemg7aN  35913  cdlemg8a  35915  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg9  35922  cdlemg11aq  35926  cdlemg10c  35927  cdlemg12a  35931  cdlemg12b  35932  cdlemg12c  35933  cdlemg17a  35949  cdlemg18b  35967  cdlemg18c  35968  cdlemg31b0a  35983  cdlemg31a  35985  cdlemg31b  35986  cdlemg31d  35988  cdlemg35  36001  trlcoabs2N  36010  trlcolem  36014  cdlemg44a  36019  trljco  36028  trljco2  36029  tendoco2  36056  tendopltp  36068  cdlemi1  36106  cdlemi2  36107  cdlemj3  36111  tendocan  36112  cdlemk3  36121  cdlemk4  36122  cdlemk5a  36123  cdlemk9  36127  cdlemk9bN  36128  cdlemkvcl  36130  cdlemk10  36131  cdlemk30  36182  cdlemk31  36184  cdlemk39  36204  cdlemkfid1N  36209  cdlemkid1  36210  cdlemkid2  36212  cdlemkfid3N  36213  cdlemk19ylem  36218  cdlemk19xlem  36230  cdlemk19x  36231  cdlemk53b  36244  cdlemk53  36245  cdlemk54  36246  cdlemk55a  36247  cdlemk43N  36251  cdlemk19u1  36257  cdlemk19u  36258  cdleml1N  36264  erngdvlem4  36279  erngdvlem4-rN  36287  dia11N  36337  cdlemm10N  36407  dib11N  36449  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505  dihord2cN  36510  dihlsscpre  36523  dih1dimb2  36530  dihvalcq2  36536  dihopelvalcpre  36537  dihord6b  36549  dih11  36554  dihmeetlem1N  36579  dihglblem2N  36583  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetcN  36591  dihmeetbclemN  36593  dihmeetlem4preN  36595  dihmeetlem9N  36604  dihmeetlem20N  36615  dihlspsnssN  36621  dihlspsnat  36622  dihatlat  36623  dihglblem6  36629  dihmeet  36632  dochss  36654  hdmapval3N  37130  hgmap11  37194  congtr  37532  fzmaxdif  37548  isnumbasgrplem2  37674  ntrclsk13  38369  ssmapsn  39408  infleinf  39588  suplesup2  39592  supxrunb3  39623  mullimc  39848  mullimcf  39855  islpcn  39871  limsupresxr  39998  liminfresxr  39999  cncfuni  40099  icccncfext  40100  stoweidlem34  40251  stoweidlem59  40276  stirlinglem13  40303  fourierdlem41  40365  fourierdlem42  40366  fourierdlem73  40396  sge0iunmptlemfi  40630  meadjiunlem  40682  ovncvrrp  40778  sssmf  40947  smflimsuplem7  41032  smflimsuplem8  41033  pfxccat3  41426  lincscm  42219  lincext3  42245  el0ldep  42255  el0ldepsnzr  42256