Theorem simp32 1208

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

Assertion

Ref	Expression
simp32	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1135	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1133	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp132  1307  simp232  1316  simp332  1325  smogt  8182  axdc3lem4  10193  bitsfzo  16123  frlmphl  20969  mdetunilem4  21745  mdetuni0  21751  mdetmul  21753  decpmatmullem  21901  logfacbnd3  26352  logexprlim  26354  log2sumbnd  26673  ax5seg  27287  numclwwlk1lem2foa  28697  iocinioc2  31079  totprob  32373  eqfunresadj  33714  nosupfv  33888  nosupres  33889  noinffv  33903  noinfres  33904  cgrtr  34273  cgrtr3  34275  ofscom  34288  cgrextend  34289  segconeq  34291  ifscgr  34325  colinearxfr  34356  brofs2  34358  brifs2  34359  fscgr  34361  btwnconn1lem2  34369  btwnconn1lem9  34376  btwnconn1lem10  34377  btwnconn1lem11  34378  btwnconn1lem12  34379  brsegle2  34390  seglecgr12im  34391  seglecgr12  34392  segletr  34395  outsideofeq  34411  ivthALT  34503  lshpkrlem5  37107  lshpkrlem6  37108  atbtwnexOLDN  37440  atbtwnex  37441  4noncolr3  37446  3dimlem3a  37453  3dim1  37460  3dim2  37461  1cvrat  37469  2atjlej  37472  hlatexch4  37474  ps-2b  37475  2atm  37520  ps-2c  37521  2atmat  37554  4atlem10  37599  4atlem11b  37601  4atlem11  37602  4at  37606  4at2  37607  2lplnja  37612  2lplnj  37613  dalemswapyz  37649  dalem-ddly  37679  cdlemb  37787  paddasslem5  37817  pmodlem1  37839  dalawlem1  37864  dalawlem3  37866  dalawlem4  37867  dalawlem5  37868  dalawlem6  37869  dalawlem7  37870  dalawlem8  37871  dalawlem9  37872  dalawlem11  37874  dalawlem12  37875  dalawlem15  37878  osumcllem5N  37953  osumcllem6N  37954  lhpexle3lem  38004  lhpmcvr4N  38019  lhpmcvr6N  38021  4atexlemex6  38067  4atex2  38070  4atex2-0bOLDN  38072  4atex2-0cOLDN  38073  ltrn11at  38140  trlval3  38180  cdlemd3  38193  cdleme7aa  38235  cdleme7b  38237  cdleme7c  38238  cdleme7d  38239  cdleme7e  38240  cdleme7ga  38241  cdleme7  38242  cdleme16aN  38252  cdleme11dN  38255  cdleme11e  38256  cdleme11l  38262  cdleme11  38263  cdleme12  38264  cdleme14  38266  cdleme15a  38267  cdleme15c  38269  cdleme16c  38273  cdleme16d  38274  cdleme16e  38275  cdleme16f  38276  cdleme17c  38281  cdleme18c  38286  cdlemeda  38291  cdlemednpq  38292  cdleme19a  38296  cdleme19c  38298  cdleme20aN  38302  cdleme20bN  38303  cdleme20l1  38313  cdleme20l2  38314  cdleme22aa  38332  cdleme22a  38333  cdleme22g  38341  cdleme23b  38343  cdleme23c  38344  cdleme26fALTN  38355  cdleme26f  38356  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme28b  38364  cdleme32b  38435  cdleme32c  38436  cdleme32e  38438  cdleme35h  38449  cdleme35sn2aw  38451  cdleme38m  38456  cdleme40n  38461  cdleme41sn3aw  38467  cdleme41sn4aw  38468  cdlemeg46gfre  38525  cdlemf1  38554  cdlemg1cex  38581  cdlemg2ce  38585  cdlemg4d  38606  cdlemg4  38610  cdlemg7fvN  38617  cdlemg8b  38621  cdlemg8c  38622  cdlemg9a  38625  cdlemg11aq  38631  cdlemg10a  38633  cdlemg12a  38636  cdlemg12b  38637  cdlemg12d  38639  cdlemg12g  38642  cdlemg12  38643  cdlemg13a  38644  cdlemg13  38645  cdlemg14f  38646  cdlemg14g  38647  cdlemg17b  38655  cdlemg17dN  38656  cdlemg17e  38658  cdlemg17pq  38665  cdlemg17iqN  38667  cdlemg18c  38673  cdlemg18d  38674  cdlemg19a  38676  cdlemg19  38677  cdlemg21  38679  cdlemg27a  38685  cdlemg28a  38686  cdlemg31b0N  38687  cdlemg27b  38689  cdlemg31c  38692  cdlemg33b0  38694  cdlemg28  38697  cdlemg33a  38699  cdlemg33  38704  cdlemg35  38706  cdlemg36  38707  cdlemg44a  38724  cdlemg46  38728  cdlemh2  38809  cdlemh  38810  cdlemj1  38814  cdlemk5  38829  cdlemk6  38830  cdlemki  38834  cdlemksv2  38840  cdlemk7  38841  cdlemk11  38842  cdlemkole  38846  cdlemk14  38847  cdlemk16  38850  cdlemk1u  38852  cdlemk18  38861  cdlemk19  38862  cdlemk7u  38863  cdlemk11u  38864  cdlemk33N  38902  cdlemkid2  38917  cdlemkfid3N  38918  cdlemk11ta  38922  cdlemk11tc  38938  cdlemk45  38940  cdlemk46  38941  cdlemk47  38942  cdlemk52  38947  cdlemk53a  38948  cdlemk54  38951  cdlemk55a  38952  cdleml1N  38969  cdleml3N  38971  cdlemn7  39196  cdlemn8  39197  cdlemn10  39199  dihordlem7  39207  dihordlem7b  39208  dihord1  39211  dihord10  39216  dihord11c  39217  dihord2  39220  hlhilphllem  39956  fmuldfeq  43078  seposep  46171  iscnrm3rlem8  46193  iscnrm3llem2  46196