Theorem simp33 1261

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

Assertion

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

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1161	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1158	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpl33OLD  1339  simpr33OLD  1357  simp133  1402  simp233  1411  simp333  1420  smogt  7700  bitsfzo  15376  frlmphl  20330  mdetunilem4  20632  mdetuni0  20638  mdetmul  20640  decpmatmullem  20789  logexprlim  25164  ax5seg  26032  iocinioc2  29868  bnj966  31337  eqfunresadj  31981  cgrtr  32420  cgrtr3  32422  ofscom  32435  segconeq  32438  btwnxfr  32484  colinearxfr  32503  fscgr  32508  btwnconn1lem1  32515  btwnconn1lem2  32516  btwnconn1lem5  32519  btwnconn1lem6  32520  btwnconn1lem8  32522  btwnconn1lem9  32523  btwnconn1lem10  32524  btwnconn1lem11  32525  btwnconn1lem12  32526  brsegle2  32537  seglecgr12im  32538  seglecgr12  32539  segletr  32542  outsideofeq  32558  lshpkrlem5  34894  lshpkrlem6  34895  atbtwnexOLDN  35227  atbtwnex  35228  4noncolr3  35233  3dimlem3a  35240  3dimlem4a  35243  3dim1  35247  3dim2  35248  1cvrat  35256  2atjlej  35259  hlatexch4  35261  ps-2b  35262  2atm  35307  ps-2c  35308  lvolex3N  35318  2atmat  35341  lvolnlelpln  35365  4atlem10  35386  4atlem11b  35388  4atlem11  35389  4at  35393  4at2  35394  2lplnja  35399  2lplnj  35400  dalemclccjdd  35468  paddasslem5  35604  paddasslem15  35614  pmodlem1  35626  dalawlem1  35651  dalawlem3  35653  dalawlem4  35654  dalawlem5  35655  dalawlem6  35656  dalawlem7  35657  dalawlem8  35658  dalawlem9  35659  dalawlem11  35661  dalawlem12  35662  dalawlem15  35665  osumcllem5N  35740  osumcllem6N  35741  lhpexle3lem  35791  lhpmcvr4N  35806  lhpmcvr6N  35808  4atexlemex6  35854  4atex2  35857  4atex2-0bOLDN  35859  4atex3  35861  ltrn11at  35927  cdlemd3  35981  cdleme7aa  36023  cdleme7b  36025  cdleme7c  36026  cdleme7d  36027  cdleme7ga  36029  cdleme16aN  36040  cdleme11dN  36043  cdleme11e  36044  cdleme11l  36050  cdleme11  36051  cdleme12  36052  cdleme14  36054  cdleme15c  36057  cdleme16b  36060  cdleme16d  36062  cdleme17b  36068  cdleme17c  36069  cdleme18c  36074  cdleme18d  36076  cdlemeda  36079  cdlemednpq  36080  cdleme19a  36084  cdleme19c  36086  cdleme20aN  36090  cdleme20bN  36091  cdleme20d  36093  cdleme20f  36095  cdleme20g  36096  cdleme20j  36099  cdleme20l1  36101  cdleme21f  36113  cdleme22aa  36120  cdleme22a  36121  cdleme22cN  36123  cdleme22e  36125  cdleme22f2  36128  cdleme22g  36129  cdleme23b  36131  cdleme23c  36132  cdleme26e  36140  cdleme26fALTN  36143  cdleme26f  36144  cdleme26f2ALTN  36145  cdleme26f2  36146  cdleme28a  36151  cdleme28b  36152  cdleme32b  36223  cdleme32c  36224  cdleme32e  36226  cdleme35h2  36238  cdleme38m  36244  cdleme41sn4aw  36256  cdlemf1  36342  cdlemg1cex  36369  cdlemg2ce  36373  cdlemg4d  36394  cdlemg4f  36396  cdlemg7fvN  36405  cdlemg8a  36408  cdlemg8b  36409  cdlemg8c  36410  cdlemg9a  36413  cdlemg11a  36418  cdlemg11aq  36419  cdlemg10a  36421  cdlemg11b  36423  cdlemg12a  36424  cdlemg12b  36425  cdlemg12d  36427  cdlemg12e  36428  cdlemg12f  36429  cdlemg12g  36430  cdlemg12  36431  cdlemg13a  36432  cdlemg13  36433  cdlemg14f  36434  cdlemg14g  36435  cdlemg17b  36443  cdlemg17dN  36444  cdlemg17e  36446  cdlemg17h  36449  cdlemg17pq  36453  cdlemg17iqN  36455  cdlemg18b  36460  cdlemg18c  36461  cdlemg18d  36462  cdlemg18  36463  cdlemg19  36465  cdlemg21  36467  cdlemg27a  36473  cdlemg31b0N  36475  cdlemg27b  36477  cdlemg33b0  36482  cdlemg33c0  36483  cdlemg28  36485  cdlemg33a  36487  cdlemg35  36494  cdlemg42  36510  cdlemg44a  36512  cdlemg47  36517  cdlemh2  36597  cdlemh  36598  cdlemj1  36602  cdlemk3  36614  cdlemk5  36617  cdlemki  36622  cdlemksv2  36628  cdlemk7  36629  cdlemk11  36630  cdlemk12  36631  cdlemkole  36634  cdlemk14  36635  cdlemk15  36636  cdlemk16a  36637  cdlemk16  36638  cdlemkj  36644  cdlemkuv2  36648  cdlemk18  36649  cdlemk19  36650  cdlemk7u  36651  cdlemk12u  36653  cdlemkoatnle-2N  36656  cdlemk13-2N  36657  cdlemkole-2N  36658  cdlemk14-2N  36659  cdlemk15-2N  36660  cdlemk16-2N  36661  cdlemk17-2N  36662  cdlemk18-2N  36667  cdlemk19-2N  36668  cdlemk7u-2N  36669  cdlemk11u-2N  36670  cdlemk12u-2N  36671  cdlemk21-2N  36672  cdlemk20-2N  36673  cdlemk22  36674  cdlemk30  36675  cdlemk31  36677  cdlemk32  36678  cdlemk24-3  36684  cdlemkid2  36705  cdlemkfid3N  36706  cdlemk45  36728  cdlemk46  36729  cdlemk47  36730  cdlemk52  36735  cdlemk53a  36736  cdleml1N  36757  cdleml3N  36759  cdlemn7  36984  cdlemn10  36987  dihordlem7  36995  dihord1  36999  dihord2a  37000  dihord10  37004  dihord11c  37005  dihord2pre2  37007  hlhilphllem  37740  fmuldfeq  40295