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  7306  smogt  8299  bitsfzo  16362  frlmphl  21736  mdetunilem4  22559  mdetuni0  22565  mdetmul  22567  decpmatmullem  22715  logexprlim  27192  noinfres  27690  ax5seg  29011  iocinioc2  32859  bnj966  35100  cgrtr  36186  cgrtr3  36188  ofscom  36201  segconeq  36204  btwnxfr  36250  colinearxfr  36269  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem12  36292  brsegle2  36303  seglecgr12im  36304  seglecgr12  36305  segletr  36308  outsideofeq  36324  lshpkrlem5  39374  lshpkrlem6  39375  atbtwnexOLDN  39707  atbtwnex  39708  4noncolr3  39713  3dimlem3a  39720  3dimlem4a  39723  3dim1  39727  3dim2  39728  1cvrat  39736  2atjlej  39739  hlatexch4  39741  ps-2b  39742  2atm  39787  ps-2c  39788  lvolex3N  39798  2atmat  39821  lvolnlelpln  39845  4atlem10  39866  4atlem11b  39868  4atlem11  39869  4at  39873  4at2  39874  2lplnja  39879  2lplnj  39880  dalemclccjdd  39948  paddasslem5  40084  paddasslem15  40094  pmodlem1  40106  dalawlem1  40131  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem11  40141  dalawlem12  40142  dalawlem15  40145  osumcllem5N  40220  osumcllem6N  40221  lhpexle3lem  40271  lhpmcvr4N  40286  lhpmcvr6N  40288  4atexlemex6  40334  4atex2  40337  4atex2-0bOLDN  40339  4atex3  40341  ltrn11at  40407  cdlemd3  40460  cdleme7aa  40502  cdleme7b  40504  cdleme7c  40505  cdleme7d  40506  cdleme7ga  40508  cdleme16aN  40519  cdleme11dN  40522  cdleme11e  40523  cdleme11l  40529  cdleme11  40530  cdleme12  40531  cdleme14  40533  cdleme15c  40536  cdleme16b  40539  cdleme16d  40541  cdleme17b  40547  cdleme17c  40548  cdleme18c  40553  cdleme18d  40555  cdlemeda  40558  cdlemednpq  40559  cdleme19a  40563  cdleme19c  40565  cdleme20aN  40569  cdleme20bN  40570  cdleme20d  40572  cdleme20f  40574  cdleme20g  40575  cdleme20j  40578  cdleme20l1  40580  cdleme21f  40592  cdleme22aa  40599  cdleme22a  40600  cdleme22cN  40602  cdleme22e  40604  cdleme22f2  40607  cdleme22g  40608  cdleme23b  40610  cdleme23c  40611  cdleme26e  40619  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme28a  40630  cdleme28b  40631  cdleme32b  40702  cdleme32c  40703  cdleme32e  40705  cdleme35h2  40717  cdleme38m  40723  cdleme41sn4aw  40735  cdlemf1  40821  cdlemg1cex  40848  cdlemg2ce  40852  cdlemg4d  40873  cdlemg4f  40875  cdlemg7fvN  40884  cdlemg8a  40887  cdlemg8b  40888  cdlemg8c  40889  cdlemg9a  40892  cdlemg11a  40897  cdlemg11aq  40898  cdlemg10a  40900  cdlemg11b  40902  cdlemg12a  40903  cdlemg12b  40904  cdlemg12d  40906  cdlemg12e  40907  cdlemg12f  40908  cdlemg12g  40909  cdlemg12  40910  cdlemg13a  40911  cdlemg13  40912  cdlemg14f  40913  cdlemg14g  40914  cdlemg17b  40922  cdlemg17dN  40923  cdlemg17e  40925  cdlemg17h  40928  cdlemg17pq  40932  cdlemg17iqN  40934  cdlemg18b  40939  cdlemg18c  40940  cdlemg18d  40941  cdlemg18  40942  cdlemg19  40944  cdlemg21  40946  cdlemg27a  40952  cdlemg31b0N  40954  cdlemg27b  40956  cdlemg33b0  40961  cdlemg33c0  40962  cdlemg28  40964  cdlemg33a  40966  cdlemg35  40973  cdlemg42  40989  cdlemg44a  40991  cdlemg47  40996  cdlemh2  41076  cdlemh  41077  cdlemj1  41081  cdlemk3  41093  cdlemk5  41096  cdlemki  41101  cdlemksv2  41107  cdlemk7  41108  cdlemk11  41109  cdlemk12  41110  cdlemkole  41113  cdlemk14  41114  cdlemk15  41115  cdlemk16a  41116  cdlemk16  41117  cdlemkj  41123  cdlemkuv2  41127  cdlemk18  41128  cdlemk19  41129  cdlemk7u  41130  cdlemk12u  41132  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk21-2N  41151  cdlemk20-2N  41152  cdlemk22  41153  cdlemk30  41154  cdlemk31  41156  cdlemk32  41157  cdlemk24-3  41163  cdlemkid2  41184  cdlemkfid3N  41185  cdlemk45  41207  cdlemk46  41208  cdlemk47  41209  cdlemk52  41214  cdlemk53a  41215  cdleml1N  41236  cdleml3N  41238  cdlemn7  41463  cdlemn10  41466  dihordlem7  41474  dihord1  41478  dihord2a  41479  dihord10  41483  dihord11c  41484  dihord2pre2  41486  hlhilphllem  42219  fmuldfeq  45829  usgrgrtrirex  48196  grlimprclnbgredg  48243  seposep  49171  iscnrm3rlem8  49192  iscnrm3llem2  49195