Theorem simp32 1211

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 1137	. 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:  simp132  1310  simp232  1319  simp332  1328  eqfunresadj  7317  smogt  8313  axdc3lem4  10382  bitsfzo  16381  frlmphl  21666  mdetunilem4  22478  mdetuni0  22484  mdetmul  22486  decpmatmullem  22634  logfacbnd3  27110  logexprlim  27112  log2sumbnd  27431  nosupfv  27594  nosupres  27595  noinffv  27609  noinfres  27610  ax5seg  28841  numclwwlk1lem2foa  30256  iocinioc2  32675  totprob  34391  cgrtr  35953  cgrtr3  35955  ofscom  35968  cgrextend  35969  segconeq  35971  ifscgr  36005  colinearxfr  36036  brofs2  36038  brifs2  36039  fscgr  36041  btwnconn1lem2  36049  btwnconn1lem9  36056  btwnconn1lem10  36057  btwnconn1lem11  36058  btwnconn1lem12  36059  brsegle2  36070  seglecgr12im  36071  seglecgr12  36072  segletr  36075  outsideofeq  36091  ivthALT  36296  lshpkrlem5  39080  lshpkrlem6  39081  atbtwnexOLDN  39414  atbtwnex  39415  4noncolr3  39420  3dimlem3a  39427  3dim1  39434  3dim2  39435  1cvrat  39443  2atjlej  39446  hlatexch4  39448  ps-2b  39449  2atm  39494  ps-2c  39495  2atmat  39528  4atlem10  39573  4atlem11b  39575  4atlem11  39576  4at  39580  4at2  39581  2lplnja  39586  2lplnj  39587  dalemswapyz  39623  dalem-ddly  39653  cdlemb  39761  paddasslem5  39791  pmodlem1  39813  dalawlem1  39838  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem15  39852  osumcllem5N  39927  osumcllem6N  39928  lhpexle3lem  39978  lhpmcvr4N  39993  lhpmcvr6N  39995  4atexlemex6  40041  4atex2  40044  4atex2-0bOLDN  40046  4atex2-0cOLDN  40047  ltrn11at  40114  trlval3  40154  cdlemd3  40167  cdleme7aa  40209  cdleme7b  40211  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme7ga  40215  cdleme7  40216  cdleme16aN  40226  cdleme11dN  40229  cdleme11e  40230  cdleme11l  40236  cdleme11  40237  cdleme12  40238  cdleme14  40240  cdleme15a  40241  cdleme15c  40243  cdleme16c  40247  cdleme16d  40248  cdleme16e  40249  cdleme16f  40250  cdleme17c  40255  cdleme18c  40260  cdlemeda  40265  cdlemednpq  40266  cdleme19a  40270  cdleme19c  40272  cdleme20aN  40276  cdleme20bN  40277  cdleme20l1  40287  cdleme20l2  40288  cdleme22aa  40306  cdleme22a  40307  cdleme22g  40315  cdleme23b  40317  cdleme23c  40318  cdleme26fALTN  40329  cdleme26f  40330  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme28b  40338  cdleme32b  40409  cdleme32c  40410  cdleme32e  40412  cdleme35h  40423  cdleme35sn2aw  40425  cdleme38m  40430  cdleme40n  40435  cdleme41sn3aw  40441  cdleme41sn4aw  40442  cdlemeg46gfre  40499  cdlemf1  40528  cdlemg1cex  40555  cdlemg2ce  40559  cdlemg4d  40580  cdlemg4  40584  cdlemg7fvN  40591  cdlemg8b  40595  cdlemg8c  40596  cdlemg9a  40599  cdlemg11aq  40605  cdlemg10a  40607  cdlemg12a  40610  cdlemg12b  40611  cdlemg12d  40613  cdlemg12g  40616  cdlemg12  40617  cdlemg13a  40618  cdlemg13  40619  cdlemg14f  40620  cdlemg14g  40621  cdlemg17b  40629  cdlemg17dN  40630  cdlemg17e  40632  cdlemg17pq  40639  cdlemg17iqN  40641  cdlemg18c  40647  cdlemg18d  40648  cdlemg19a  40650  cdlemg19  40651  cdlemg21  40653  cdlemg27a  40659  cdlemg28a  40660  cdlemg31b0N  40661  cdlemg27b  40663  cdlemg31c  40666  cdlemg33b0  40668  cdlemg28  40671  cdlemg33a  40673  cdlemg33  40678  cdlemg35  40680  cdlemg36  40681  cdlemg44a  40698  cdlemg46  40702  cdlemh2  40783  cdlemh  40784  cdlemj1  40788  cdlemk5  40803  cdlemk6  40804  cdlemki  40808  cdlemksv2  40814  cdlemk7  40815  cdlemk11  40816  cdlemkole  40820  cdlemk14  40821  cdlemk16  40824  cdlemk1u  40826  cdlemk18  40835  cdlemk19  40836  cdlemk7u  40837  cdlemk11u  40838  cdlemk33N  40876  cdlemkid2  40891  cdlemkfid3N  40892  cdlemk11ta  40896  cdlemk11tc  40912  cdlemk45  40914  cdlemk46  40915  cdlemk47  40916  cdlemk52  40921  cdlemk53a  40922  cdlemk54  40925  cdlemk55a  40926  cdleml1N  40943  cdleml3N  40945  cdlemn7  41170  cdlemn8  41171  cdlemn10  41173  dihordlem7  41181  dihordlem7b  41182  dihord1  41185  dihord10  41190  dihord11c  41191  dihord2  41194  hlhilphllem  41926  fmuldfeq  45554  seposep  48887  iscnrm3rlem8  48908  iscnrm3llem2  48911