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  7352  smogt  8379  bitsfzo  16452  frlmphl  21739  mdetunilem4  22551  mdetuni0  22557  mdetmul  22559  decpmatmullem  22707  logexprlim  27186  noinfres  27684  ax5seg  28863  iocinioc2  32702  bnj966  34921  cgrtr  35956  cgrtr3  35958  ofscom  35971  segconeq  35974  btwnxfr  36020  colinearxfr  36039  fscgr  36044  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem12  36062  brsegle2  36073  seglecgr12im  36074  seglecgr12  36075  segletr  36078  outsideofeq  36094  lshpkrlem5  39078  lshpkrlem6  39079  atbtwnexOLDN  39412  atbtwnex  39413  4noncolr3  39418  3dimlem3a  39425  3dimlem4a  39428  3dim1  39432  3dim2  39433  1cvrat  39441  2atjlej  39444  hlatexch4  39446  ps-2b  39447  2atm  39492  ps-2c  39493  lvolex3N  39503  2atmat  39526  lvolnlelpln  39550  4atlem10  39571  4atlem11b  39573  4atlem11  39574  4at  39578  4at2  39579  2lplnja  39584  2lplnj  39585  dalemclccjdd  39653  paddasslem5  39789  paddasslem15  39799  pmodlem1  39811  dalawlem1  39836  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem15  39850  osumcllem5N  39925  osumcllem6N  39926  lhpexle3lem  39976  lhpmcvr4N  39991  lhpmcvr6N  39993  4atexlemex6  40039  4atex2  40042  4atex2-0bOLDN  40044  4atex3  40046  ltrn11at  40112  cdlemd3  40165  cdleme7aa  40207  cdleme7b  40209  cdleme7c  40210  cdleme7d  40211  cdleme7ga  40213  cdleme16aN  40224  cdleme11dN  40227  cdleme11e  40228  cdleme11l  40234  cdleme11  40235  cdleme12  40236  cdleme14  40238  cdleme15c  40241  cdleme16b  40244  cdleme16d  40246  cdleme17b  40252  cdleme17c  40253  cdleme18c  40258  cdleme18d  40260  cdlemeda  40263  cdlemednpq  40264  cdleme19a  40268  cdleme19c  40270  cdleme20aN  40274  cdleme20bN  40275  cdleme20d  40277  cdleme20f  40279  cdleme20g  40280  cdleme20j  40283  cdleme20l1  40285  cdleme21f  40297  cdleme22aa  40304  cdleme22a  40305  cdleme22cN  40307  cdleme22e  40309  cdleme22f2  40312  cdleme22g  40313  cdleme23b  40315  cdleme23c  40316  cdleme26e  40324  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme28a  40335  cdleme28b  40336  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme35h2  40422  cdleme38m  40428  cdleme41sn4aw  40440  cdlemf1  40526  cdlemg1cex  40553  cdlemg2ce  40557  cdlemg4d  40578  cdlemg4f  40580  cdlemg7fvN  40589  cdlemg8a  40592  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg11a  40602  cdlemg11aq  40603  cdlemg10a  40605  cdlemg11b  40607  cdlemg12a  40608  cdlemg12b  40609  cdlemg12d  40611  cdlemg12e  40612  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg14f  40618  cdlemg14g  40619  cdlemg17b  40627  cdlemg17dN  40628  cdlemg17e  40630  cdlemg17h  40633  cdlemg17pq  40637  cdlemg17iqN  40639  cdlemg18b  40644  cdlemg18c  40645  cdlemg18d  40646  cdlemg18  40647  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg33b0  40666  cdlemg33c0  40667  cdlemg28  40669  cdlemg33a  40671  cdlemg35  40678  cdlemg42  40694  cdlemg44a  40696  cdlemg47  40701  cdlemh2  40781  cdlemh  40782  cdlemj1  40786  cdlemk3  40798  cdlemk5  40801  cdlemki  40806  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  cdlemkj  40828  cdlemkuv2  40832  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk12u  40837  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk7u-2N  40853  cdlemk11u-2N  40854  cdlemk12u-2N  40855  cdlemk21-2N  40856  cdlemk20-2N  40857  cdlemk22  40858  cdlemk30  40859  cdlemk31  40861  cdlemk32  40862  cdlemk24-3  40868  cdlemkid2  40889  cdlemkfid3N  40890  cdlemk45  40912  cdlemk46  40913  cdlemk47  40914  cdlemk52  40919  cdlemk53a  40920  cdleml1N  40941  cdleml3N  40943  cdlemn7  41168  cdlemn10  41171  dihordlem7  41179  dihord1  41183  dihord2a  41184  dihord10  41188  dihord11c  41189  dihord2pre2  41191  hlhilphllem  41924  fmuldfeq  45560  usgrgrtrirex  47910  seposep  48848  iscnrm3rlem8  48869  iscnrm3llem2  48872