Theorem simp32 1206

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp132  1305  simp232  1314  simp332  1323  smogt  7998  axdc3lem4  9869  bitsfzo  15778  frlmphl  20919  mdetunilem4  21218  mdetuni0  21224  mdetmul  21226  decpmatmullem  21373  logfacbnd3  25793  logexprlim  25795  log2sumbnd  26114  ax5seg  26718  numclwwlk1lem2foa  28127  iocinioc2  30496  totprob  31680  eqfunresadj  32999  nosupfv  33201  nosupres  33202  cgrtr  33448  cgrtr3  33450  ofscom  33463  cgrextend  33464  segconeq  33466  ifscgr  33500  colinearxfr  33531  brofs2  33533  brifs2  33534  fscgr  33536  btwnconn1lem2  33544  btwnconn1lem9  33551  btwnconn1lem10  33552  btwnconn1lem11  33553  btwnconn1lem12  33554  brsegle2  33565  seglecgr12im  33566  seglecgr12  33567  segletr  33570  outsideofeq  33586  ivthALT  33678  lshpkrlem5  36244  lshpkrlem6  36245  atbtwnexOLDN  36577  atbtwnex  36578  4noncolr3  36583  3dimlem3a  36590  3dim1  36597  3dim2  36598  1cvrat  36606  2atjlej  36609  hlatexch4  36611  ps-2b  36612  2atm  36657  ps-2c  36658  2atmat  36691  4atlem10  36736  4atlem11b  36738  4atlem11  36739  4at  36743  4at2  36744  2lplnja  36749  2lplnj  36750  dalemswapyz  36786  dalem-ddly  36816  cdlemb  36924  paddasslem5  36954  pmodlem1  36976  dalawlem1  37001  dalawlem3  37003  dalawlem4  37004  dalawlem5  37005  dalawlem6  37006  dalawlem7  37007  dalawlem8  37008  dalawlem9  37009  dalawlem11  37011  dalawlem12  37012  dalawlem15  37015  osumcllem5N  37090  osumcllem6N  37091  lhpexle3lem  37141  lhpmcvr4N  37156  lhpmcvr6N  37158  4atexlemex6  37204  4atex2  37207  4atex2-0bOLDN  37209  4atex2-0cOLDN  37210  ltrn11at  37277  trlval3  37317  cdlemd3  37330  cdleme7aa  37372  cdleme7b  37374  cdleme7c  37375  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme16aN  37389  cdleme11dN  37392  cdleme11e  37393  cdleme11l  37399  cdleme11  37400  cdleme12  37401  cdleme14  37403  cdleme15a  37404  cdleme15c  37406  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme17c  37418  cdleme18c  37423  cdlemeda  37428  cdlemednpq  37429  cdleme19a  37433  cdleme19c  37435  cdleme20aN  37439  cdleme20bN  37440  cdleme20l1  37450  cdleme20l2  37451  cdleme22aa  37469  cdleme22a  37470  cdleme22g  37478  cdleme23b  37480  cdleme23c  37481  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme28b  37501  cdleme32b  37572  cdleme32c  37573  cdleme32e  37575  cdleme35h  37586  cdleme35sn2aw  37588  cdleme38m  37593  cdleme40n  37598  cdleme41sn3aw  37604  cdleme41sn4aw  37605  cdlemeg46gfre  37662  cdlemf1  37691  cdlemg1cex  37718  cdlemg2ce  37722  cdlemg4d  37743  cdlemg4  37747  cdlemg7fvN  37754  cdlemg8b  37758  cdlemg8c  37759  cdlemg9a  37762  cdlemg11aq  37768  cdlemg10a  37770  cdlemg12a  37773  cdlemg12b  37774  cdlemg12d  37776  cdlemg12g  37779  cdlemg12  37780  cdlemg13a  37781  cdlemg13  37782  cdlemg14f  37783  cdlemg14g  37784  cdlemg17b  37792  cdlemg17dN  37793  cdlemg17e  37795  cdlemg17pq  37802  cdlemg17iqN  37804  cdlemg18c  37810  cdlemg18d  37811  cdlemg19a  37813  cdlemg19  37814  cdlemg21  37816  cdlemg27a  37822  cdlemg28a  37823  cdlemg31b0N  37824  cdlemg27b  37826  cdlemg31c  37829  cdlemg33b0  37831  cdlemg28  37834  cdlemg33a  37836  cdlemg33  37841  cdlemg35  37843  cdlemg36  37844  cdlemg44a  37861  cdlemg46  37865  cdlemh2  37946  cdlemh  37947  cdlemj1  37951  cdlemk5  37966  cdlemk6  37967  cdlemki  37971  cdlemksv2  37977  cdlemk7  37978  cdlemk11  37979  cdlemkole  37983  cdlemk14  37984  cdlemk16  37987  cdlemk1u  37989  cdlemk18  37998  cdlemk19  37999  cdlemk7u  38000  cdlemk11u  38001  cdlemk33N  38039  cdlemkid2  38054  cdlemkfid3N  38055  cdlemk11ta  38059  cdlemk11tc  38075  cdlemk45  38077  cdlemk46  38078  cdlemk47  38079  cdlemk52  38084  cdlemk53a  38085  cdlemk54  38088  cdlemk55a  38089  cdleml1N  38106  cdleml3N  38108  cdlemn7  38333  cdlemn8  38334  cdlemn10  38336  dihordlem7  38344  dihordlem7b  38345  dihord1  38348  dihord10  38353  dihord11c  38354  dihord2  38357  hlhilphllem  39089  fmuldfeq  41857