Theorem simp32 1260

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 1160	. 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:  simpl32OLD  1337  simpr32OLD  1355  simp132  1401  simp232  1410  simp332  1419  smogt  7703  axdc3lem4  9563  bitsfzo  15379  frlmphl  20334  mdetunilem4  20636  mdetuni0  20642  mdetmul  20644  decpmatmullem  20793  logfacbnd3  25168  logexprlim  25170  log2sumbnd  25453  ax5seg  26038  numclwwlk1lem2foa  27539  iocinioc2  29874  totprob  30820  eqfunresadj  31986  nosupfv  32178  nosupres  32179  cgrtr  32425  cgrtr3  32427  ofscom  32440  cgrextend  32441  segconeq  32443  ifscgr  32477  colinearxfr  32508  brofs2  32510  brifs2  32511  fscgr  32513  btwnconn1lem2  32521  btwnconn1lem9  32528  btwnconn1lem10  32529  btwnconn1lem11  32530  btwnconn1lem12  32531  brsegle2  32542  seglecgr12im  32543  seglecgr12  32544  segletr  32547  outsideofeq  32563  ivthALT  32656  lshpkrlem5  34896  lshpkrlem6  34897  atbtwnexOLDN  35229  atbtwnex  35230  4noncolr3  35235  3dimlem3a  35242  3dim1  35249  3dim2  35250  1cvrat  35258  2atjlej  35261  hlatexch4  35263  ps-2b  35264  2atm  35309  ps-2c  35310  2atmat  35343  4atlem10  35388  4atlem11b  35390  4atlem11  35391  4at  35395  4at2  35396  2lplnja  35401  2lplnj  35402  dalemswapyz  35438  dalem-ddly  35468  cdlemb  35576  paddasslem5  35606  pmodlem1  35628  dalawlem1  35653  dalawlem3  35655  dalawlem4  35656  dalawlem5  35657  dalawlem6  35658  dalawlem7  35659  dalawlem8  35660  dalawlem9  35661  dalawlem11  35663  dalawlem12  35664  dalawlem15  35667  osumcllem5N  35742  osumcllem6N  35743  lhpexle3lem  35793  lhpmcvr4N  35808  lhpmcvr6N  35810  4atexlemex6  35856  4atex2  35859  4atex2-0bOLDN  35861  4atex2-0cOLDN  35862  ltrn11at  35929  trlval3  35969  cdlemd3  35982  cdleme7aa  36024  cdleme7b  36026  cdleme7c  36027  cdleme7d  36028  cdleme7e  36029  cdleme7ga  36030  cdleme7  36031  cdleme16aN  36041  cdleme11dN  36044  cdleme11e  36045  cdleme11l  36051  cdleme11  36052  cdleme12  36053  cdleme14  36055  cdleme15a  36056  cdleme15c  36058  cdleme16c  36062  cdleme16d  36063  cdleme16e  36064  cdleme16f  36065  cdleme17c  36070  cdleme18c  36075  cdlemeda  36080  cdlemednpq  36081  cdleme19a  36085  cdleme19c  36087  cdleme20aN  36091  cdleme20bN  36092  cdleme20l1  36102  cdleme20l2  36103  cdleme22aa  36121  cdleme22a  36122  cdleme22g  36130  cdleme23b  36132  cdleme23c  36133  cdleme26fALTN  36144  cdleme26f  36145  cdleme26f2ALTN  36146  cdleme26f2  36147  cdleme28b  36153  cdleme32b  36224  cdleme32c  36225  cdleme32e  36227  cdleme35h  36238  cdleme35sn2aw  36240  cdleme38m  36245  cdleme40n  36250  cdleme41sn3aw  36256  cdleme41sn4aw  36257  cdlemeg46gfre  36314  cdlemf1  36343  cdlemg1cex  36370  cdlemg2ce  36374  cdlemg4d  36395  cdlemg4  36399  cdlemg7fvN  36406  cdlemg8b  36410  cdlemg8c  36411  cdlemg9a  36414  cdlemg11aq  36420  cdlemg10a  36422  cdlemg12a  36425  cdlemg12b  36426  cdlemg12d  36428  cdlemg12g  36431  cdlemg12  36432  cdlemg13a  36433  cdlemg13  36434  cdlemg14f  36435  cdlemg14g  36436  cdlemg17b  36444  cdlemg17dN  36445  cdlemg17e  36447  cdlemg17pq  36454  cdlemg17iqN  36456  cdlemg18c  36462  cdlemg18d  36463  cdlemg19a  36465  cdlemg19  36466  cdlemg21  36468  cdlemg27a  36474  cdlemg28a  36475  cdlemg31b0N  36476  cdlemg27b  36478  cdlemg31c  36481  cdlemg33b0  36483  cdlemg28  36486  cdlemg33a  36488  cdlemg33  36493  cdlemg35  36495  cdlemg36  36496  cdlemg44a  36513  cdlemg46  36517  cdlemh2  36598  cdlemh  36599  cdlemj1  36603  cdlemk5  36618  cdlemk6  36619  cdlemki  36623  cdlemksv2  36629  cdlemk7  36630  cdlemk11  36631  cdlemkole  36635  cdlemk14  36636  cdlemk16  36639  cdlemk1u  36641  cdlemk18  36650  cdlemk19  36651  cdlemk7u  36652  cdlemk11u  36653  cdlemk33N  36691  cdlemkid2  36706  cdlemkfid3N  36707  cdlemk11ta  36711  cdlemk11tc  36727  cdlemk45  36729  cdlemk46  36730  cdlemk47  36731  cdlemk52  36736  cdlemk53a  36737  cdlemk54  36740  cdlemk55a  36741  cdleml1N  36758  cdleml3N  36760  cdlemn7  36985  cdlemn8  36986  cdlemn10  36988  dihordlem7  36996  dihordlem7b  36997  dihord1  37000  dihord10  37005  dihord11c  37006  dihord2  37009  hlhilphllem  37741  fmuldfeq  40296