Theorem simp33 1212

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 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1135	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp133  1311  simp233  1320  simp333  1329  eqfunresadj  7303  smogt  8296  bitsfzo  16353  frlmphl  21727  mdetunilem4  22550  mdetuni0  22556  mdetmul  22558  decpmatmullem  22706  logexprlim  27183  noinfres  27681  ax5seg  28937  iocinioc2  32787  bnj966  35028  cgrtr  36108  cgrtr3  36110  ofscom  36123  segconeq  36126  btwnxfr  36172  colinearxfr  36191  fscgr  36196  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem5  36207  btwnconn1lem6  36208  btwnconn1lem8  36210  btwnconn1lem9  36211  btwnconn1lem10  36212  btwnconn1lem11  36213  btwnconn1lem12  36214  brsegle2  36225  seglecgr12im  36226  seglecgr12  36227  segletr  36230  outsideofeq  36246  lshpkrlem5  39286  lshpkrlem6  39287  atbtwnexOLDN  39619  atbtwnex  39620  4noncolr3  39625  3dimlem3a  39632  3dimlem4a  39635  3dim1  39639  3dim2  39640  1cvrat  39648  2atjlej  39651  hlatexch4  39653  ps-2b  39654  2atm  39699  ps-2c  39700  lvolex3N  39710  2atmat  39733  lvolnlelpln  39757  4atlem10  39778  4atlem11b  39780  4atlem11  39781  4at  39785  4at2  39786  2lplnja  39791  2lplnj  39792  dalemclccjdd  39860  paddasslem5  39996  paddasslem15  40006  pmodlem1  40018  dalawlem1  40043  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem15  40057  osumcllem5N  40132  osumcllem6N  40133  lhpexle3lem  40183  lhpmcvr4N  40198  lhpmcvr6N  40200  4atexlemex6  40246  4atex2  40249  4atex2-0bOLDN  40251  4atex3  40253  ltrn11at  40319  cdlemd3  40372  cdleme7aa  40414  cdleme7b  40416  cdleme7c  40417  cdleme7d  40418  cdleme7ga  40420  cdleme16aN  40431  cdleme11dN  40434  cdleme11e  40435  cdleme11l  40441  cdleme11  40442  cdleme12  40443  cdleme14  40445  cdleme15c  40448  cdleme16b  40451  cdleme16d  40453  cdleme17b  40459  cdleme17c  40460  cdleme18c  40465  cdleme18d  40467  cdlemeda  40470  cdlemednpq  40471  cdleme19a  40475  cdleme19c  40477  cdleme20aN  40481  cdleme20bN  40482  cdleme20d  40484  cdleme20f  40486  cdleme20g  40487  cdleme20j  40490  cdleme20l1  40492  cdleme21f  40504  cdleme22aa  40511  cdleme22a  40512  cdleme22cN  40514  cdleme22e  40516  cdleme22f2  40519  cdleme22g  40520  cdleme23b  40522  cdleme23c  40523  cdleme26e  40531  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme28a  40542  cdleme28b  40543  cdleme32b  40614  cdleme32c  40615  cdleme32e  40617  cdleme35h2  40629  cdleme38m  40635  cdleme41sn4aw  40647  cdlemf1  40733  cdlemg1cex  40760  cdlemg2ce  40764  cdlemg4d  40785  cdlemg4f  40787  cdlemg7fvN  40796  cdlemg8a  40799  cdlemg8b  40800  cdlemg8c  40801  cdlemg9a  40804  cdlemg11a  40809  cdlemg11aq  40810  cdlemg10a  40812  cdlemg11b  40814  cdlemg12a  40815  cdlemg12b  40816  cdlemg12d  40818  cdlemg12e  40819  cdlemg12f  40820  cdlemg12g  40821  cdlemg12  40822  cdlemg13a  40823  cdlemg13  40824  cdlemg14f  40825  cdlemg14g  40826  cdlemg17b  40834  cdlemg17dN  40835  cdlemg17e  40837  cdlemg17h  40840  cdlemg17pq  40844  cdlemg17iqN  40846  cdlemg18b  40851  cdlemg18c  40852  cdlemg18d  40853  cdlemg18  40854  cdlemg19  40856  cdlemg21  40858  cdlemg27a  40864  cdlemg31b0N  40866  cdlemg27b  40868  cdlemg33b0  40873  cdlemg33c0  40874  cdlemg28  40876  cdlemg33a  40878  cdlemg35  40885  cdlemg42  40901  cdlemg44a  40903  cdlemg47  40908  cdlemh2  40988  cdlemh  40989  cdlemj1  40993  cdlemk3  41005  cdlemk5  41008  cdlemki  41013  cdlemksv2  41019  cdlemk7  41020  cdlemk11  41021  cdlemk12  41022  cdlemkole  41025  cdlemk14  41026  cdlemk15  41027  cdlemk16a  41028  cdlemk16  41029  cdlemkj  41035  cdlemkuv2  41039  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk12u  41044  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk7u-2N  41060  cdlemk11u-2N  41061  cdlemk12u-2N  41062  cdlemk21-2N  41063  cdlemk20-2N  41064  cdlemk22  41065  cdlemk30  41066  cdlemk31  41068  cdlemk32  41069  cdlemk24-3  41075  cdlemkid2  41096  cdlemkfid3N  41097  cdlemk45  41119  cdlemk46  41120  cdlemk47  41121  cdlemk52  41126  cdlemk53a  41127  cdleml1N  41148  cdleml3N  41150  cdlemn7  41375  cdlemn10  41378  dihordlem7  41386  dihord1  41390  dihord2a  41391  dihord10  41395  dihord11c  41396  dihord2pre2  41398  hlhilphllem  42131  fmuldfeq  45745  usgrgrtrirex  48112  grlimprclnbgredg  48159  seposep  49087  iscnrm3rlem8  49108  iscnrm3llem2  49111