Theorem simp32 1210

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 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp132  1309  simp232  1318  simp332  1327  eqfunresadj  7310  smogt  8318  axdc3lem4  10398  bitsfzo  16326  frlmphl  21224  mdetunilem4  22001  mdetuni0  22007  mdetmul  22009  decpmatmullem  22157  logfacbnd3  26608  logexprlim  26610  log2sumbnd  26929  nosupfv  27091  nosupres  27092  noinffv  27106  noinfres  27107  ax5seg  27950  numclwwlk1lem2foa  29361  iocinioc2  31750  totprob  33116  cgrtr  34653  cgrtr3  34655  ofscom  34668  cgrextend  34669  segconeq  34671  ifscgr  34705  colinearxfr  34736  brofs2  34738  brifs2  34739  fscgr  34741  btwnconn1lem2  34749  btwnconn1lem9  34756  btwnconn1lem10  34757  btwnconn1lem11  34758  btwnconn1lem12  34759  brsegle2  34770  seglecgr12im  34771  seglecgr12  34772  segletr  34775  outsideofeq  34791  ivthALT  34883  lshpkrlem5  37649  lshpkrlem6  37650  atbtwnexOLDN  37983  atbtwnex  37984  4noncolr3  37989  3dimlem3a  37996  3dim1  38003  3dim2  38004  1cvrat  38012  2atjlej  38015  hlatexch4  38017  ps-2b  38018  2atm  38063  ps-2c  38064  2atmat  38097  4atlem10  38142  4atlem11b  38144  4atlem11  38145  4at  38149  4at2  38150  2lplnja  38155  2lplnj  38156  dalemswapyz  38192  dalem-ddly  38222  cdlemb  38330  paddasslem5  38360  pmodlem1  38382  dalawlem1  38407  dalawlem3  38409  dalawlem4  38410  dalawlem5  38411  dalawlem6  38412  dalawlem7  38413  dalawlem8  38414  dalawlem9  38415  dalawlem11  38417  dalawlem12  38418  dalawlem15  38421  osumcllem5N  38496  osumcllem6N  38497  lhpexle3lem  38547  lhpmcvr4N  38562  lhpmcvr6N  38564  4atexlemex6  38610  4atex2  38613  4atex2-0bOLDN  38615  4atex2-0cOLDN  38616  ltrn11at  38683  trlval3  38723  cdlemd3  38736  cdleme7aa  38778  cdleme7b  38780  cdleme7c  38781  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme7  38785  cdleme16aN  38795  cdleme11dN  38798  cdleme11e  38799  cdleme11l  38805  cdleme11  38806  cdleme12  38807  cdleme14  38809  cdleme15a  38810  cdleme15c  38812  cdleme16c  38816  cdleme16d  38817  cdleme16e  38818  cdleme16f  38819  cdleme17c  38824  cdleme18c  38829  cdlemeda  38834  cdlemednpq  38835  cdleme19a  38839  cdleme19c  38841  cdleme20aN  38845  cdleme20bN  38846  cdleme20l1  38856  cdleme20l2  38857  cdleme22aa  38875  cdleme22a  38876  cdleme22g  38884  cdleme23b  38886  cdleme23c  38887  cdleme26fALTN  38898  cdleme26f  38899  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme28b  38907  cdleme32b  38978  cdleme32c  38979  cdleme32e  38981  cdleme35h  38992  cdleme35sn2aw  38994  cdleme38m  38999  cdleme40n  39004  cdleme41sn3aw  39010  cdleme41sn4aw  39011  cdlemeg46gfre  39068  cdlemf1  39097  cdlemg1cex  39124  cdlemg2ce  39128  cdlemg4d  39149  cdlemg4  39153  cdlemg7fvN  39160  cdlemg8b  39164  cdlemg8c  39165  cdlemg9a  39168  cdlemg11aq  39174  cdlemg10a  39176  cdlemg12a  39179  cdlemg12b  39180  cdlemg12d  39182  cdlemg12g  39185  cdlemg12  39186  cdlemg13a  39187  cdlemg13  39188  cdlemg14f  39189  cdlemg14g  39190  cdlemg17b  39198  cdlemg17dN  39199  cdlemg17e  39201  cdlemg17pq  39208  cdlemg17iqN  39210  cdlemg18c  39216  cdlemg18d  39217  cdlemg19a  39219  cdlemg19  39220  cdlemg21  39222  cdlemg27a  39228  cdlemg28a  39229  cdlemg31b0N  39230  cdlemg27b  39232  cdlemg31c  39235  cdlemg33b0  39237  cdlemg28  39240  cdlemg33a  39242  cdlemg33  39247  cdlemg35  39249  cdlemg36  39250  cdlemg44a  39267  cdlemg46  39271  cdlemh2  39352  cdlemh  39353  cdlemj1  39357  cdlemk5  39372  cdlemk6  39373  cdlemki  39377  cdlemksv2  39383  cdlemk7  39384  cdlemk11  39385  cdlemkole  39389  cdlemk14  39390  cdlemk16  39393  cdlemk1u  39395  cdlemk18  39404  cdlemk19  39405  cdlemk7u  39406  cdlemk11u  39407  cdlemk33N  39445  cdlemkid2  39460  cdlemkfid3N  39461  cdlemk11ta  39465  cdlemk11tc  39481  cdlemk45  39483  cdlemk46  39484  cdlemk47  39485  cdlemk52  39490  cdlemk53a  39491  cdlemk54  39494  cdlemk55a  39495  cdleml1N  39512  cdleml3N  39514  cdlemn7  39739  cdlemn8  39740  cdlemn10  39742  dihordlem7  39750  dihordlem7b  39751  dihord1  39754  dihord10  39759  dihord11c  39760  dihord2  39763  hlhilphllem  40499  fmuldfeq  43944  seposep  47078  iscnrm3rlem8  47100  iscnrm3llem2  47103