Theorem simp21 1206

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp21	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp21

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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:  simp121  1305  simp221  1314  simp321  1323  omeulem1  8578  cofsmo  10260  axdc4lem  10446  0catg  17628  funcoppc  17821  funcres  17842  catcisolem  18056  1stfcl  18145  2ndfcl  18146  prfcl  18151  evlfcl  18171  curf1cl  18177  curfcl  18181  hofcl  18208  mulgdirlem  18979  mdetunilem4  22108  mdetuni0  22114  mdetmul  22116  prdsxmetlem  23865  isosctrlem3  26314  isosctr  26315  amgmlem  26483  nosupbnd2lem1  27207  addsass  27477  f1otrg  28111  colinearalg  28157  ax5seglem6  28181  ax5seg  28185  axpasch  28188  axeuclidlem  28209  axeuclid  28210  uhgr2edg  28454  numclwlk1lem2  29612  ogrpsub  32221  ogrpaddlt  32222  ogrpsublt  32226  rhmdvd  32424  bnj1128  33989  mclspps  34563  cgrtr  34952  cgrtr3  34954  ofscom  34967  segconeq  34970  ifscgr  35004  btwnxfr  35016  colinearxfr  35035  lineext  35036  brofs2  35037  brifs2  35038  fscgr  35040  linecgr  35041  btwnconn1lem1  35047  btwnconn1lem2  35048  btwnconn1lem3  35049  btwnconn1lem4  35050  btwnconn1lem5  35051  btwnconn1lem6  35052  btwnconn1lem7  35053  seglecgr12im  35070  seglecgr12  35071  segletr  35074  broutsideof3  35086  outsideofeq  35090  lineunray  35107  lineelsb2  35108  linecom  35110  lshpkrlem5  37972  omlmod1i2N  38118  cvrnbtwn3  38134  cvrcmp  38141  cvrcmp2  38142  cvlexch2  38187  cvlexchb2  38189  cvlatexchb2  38193  cvlatexch2  38195  cvlatexch3  38196  cvlsupr7  38206  atnlej1  38238  atnlej2  38239  2llnneN  38268  cvratlem  38280  atcvrneN  38289  atcvrj1  38290  atlelt  38297  2atjm  38304  3noncolr2  38308  3noncolr1N  38309  3dimlem2  38318  3dim1  38326  3dim2  38327  1cvrat  38335  ps-1  38336  ps-2  38337  2atjlej  38338  hlatexch3N  38339  ps-2b  38341  3atlem1  38342  3atlem2  38343  3atlem5  38346  3atlem6  38347  llnle  38377  2atm  38386  ps-2c  38387  lplni2  38396  lplnle  38399  lplnnle2at  38400  lplnri3N  38414  llncvrlpln2  38416  2atmat  38420  2llnm2N  38427  2llnm4  38429  2llnmeqat  38430  lvolnle3at  38441  4atlem0ae  38453  4atlem0be  38454  4atlem3b  38457  4atlem9  38462  4atlem10a  38463  4atlem10  38465  4atlem11a  38466  4atlem12a  38469  4at2  38473  2lplnm2N  38480  lneq2at  38637  2llnma1b  38645  2llnma1  38646  2llnma3r  38647  2llnma2  38648  2llnma2rN  38649  cdlema1N  38650  paddasslem2  38680  paddasslem15  38693  paddasslem16  38694  pmodlem1  38705  pmodlem2  38706  pmod2iN  38708  hlmod1i  38715  atmod1i1m  38717  atmod2i1  38720  atmod2i2  38721  atmod3i1  38723  atmod3i2  38724  atmod4i1  38725  atmod4i2  38726  llnexchb2lem  38727  llnexch2N  38729  dalawlem3  38732  dalawlem4  38733  dalawlem5  38734  dalawlem6  38735  dalawlem7  38736  dalawlem8  38737  dalawlem9  38738  dalawlem11  38740  dalawlem12  38741  dalawlem13  38742  dalawlem15  38744  osumcllem9N  38823  pl42lem1N  38838  4atexlems  38911  4atex2  38936  4atex2-0bOLDN  38938  trlval4  39047  cdlemc5  39054  cdlemc6  39055  cdlemd2  39058  cdlemd4  39060  cdlemd6  39062  cdleme00a  39068  cdleme0e  39076  cdleme3g  39093  cdleme3h  39094  cdleme3  39096  cdleme4  39097  cdleme4a  39098  cdleme5  39099  cdleme9  39112  cdleme16aN  39118  cdleme11c  39120  cdleme11e  39122  cdleme11g  39124  cdleme11h  39125  cdleme11j  39126  cdleme11k  39127  cdleme11l  39128  cdleme11  39129  cdleme12  39130  cdleme14  39132  cdleme15c  39135  cdleme16b  39138  cdleme16c  39139  cdleme16d  39140  cdleme16e  39141  cdleme16f  39142  cdleme0nex  39149  cdleme18a  39150  cdleme18c  39152  cdleme18d  39154  cdlemednpq  39158  cdlemednuN  39159  cdleme20zN  39160  cdleme20y  39161  cdleme19a  39162  cdleme19b  39163  cdleme19d  39165  cdleme19e  39166  cdleme20aN  39168  cdleme20bN  39169  cdleme20c  39170  cdleme20d  39171  cdleme20f  39173  cdleme20g  39174  cdleme20i  39176  cdleme20j  39177  cdleme20l1  39179  cdleme20l2  39180  cdleme20l  39181  cdleme20m  39182  cdleme21b  39185  cdleme21c  39186  cdleme21e  39190  cdleme21f  39191  cdleme22a  39199  cdleme22b  39200  cdleme22e  39203  cdleme22eALTN  39204  cdleme22f  39205  cdleme26eALTN  39220  cdleme26fALTN  39221  cdleme26f  39222  cdleme26f2ALTN  39223  cdleme26f2  39224  cdleme27N  39228  cdleme28a  39229  cdleme28b  39230  cdleme30a  39237  cdleme43fsv1snlem  39279  cdlemefs31fv1  39283  cdlemefs45eN  39290  cdleme32b  39301  cdleme32c  39302  cdleme32d  39303  cdleme35h  39315  cdleme36a  39319  cdleme36m  39320  cdleme37m  39321  cdleme40m  39326  cdleme40n  39327  cdleme41sn3aw  39333  cdleme41sn4aw  39334  cdleme41fva11  39336  cdleme42k  39343  cdleme43cN  39350  cdleme43dN  39351  cdleme46f2g1  39353  cdlemeg47rv2  39369  cdlemeg46sfg  39379  cdlemeg46fjgN  39380  cdlemeg46rjgN  39381  cdlemeg46fjv  39382  cdlemeg46frv  39384  cdlemeg46vrg  39386  cdlemeg46rgv  39387  cdlemeg46req  39388  cdlemeg46gfv  39389  cdlemg4a  39467  cdlemg4d  39472  cdlemg4e  39473  cdlemg4f  39474  cdlemg4g  39475  cdlemg4  39476  cdlemg6d  39480  cdlemg6e  39481  cdlemg8b  39487  cdlemg8c  39488  cdlemg9a  39491  cdlemg9b  39492  cdlemg10a  39499  cdlemg10  39500  cdlemg12a  39502  cdlemg12b  39503  cdlemg12f  39507  cdlemg12g  39508  cdlemg12  39509  cdlemg17dN  39522  cdlemg17dALTN  39523  cdlemg17e  39524  cdlemg17f  39525  cdlemg17g  39526  cdlemg17h  39527  cdlemg17i  39528  cdlemg17pq  39531  cdlemg17iqN  39533  cdlemg17  39536  cdlemg18b  39538  cdlemg18c  39539  cdlemg19a  39542  cdlemg19  39543  cdlemg28a  39552  cdlemg27b  39555  cdlemg28b  39562  cdlemg28  39563  cdlemg33a  39565  cdlemg33b  39566  cdlemg33c  39567  cdlemg33d  39568  cdlemg33e  39569  cdlemg33  39570  cdlemg35  39572  cdlemg36  39573  cdlemg44a  39590  cdlemh  39676  cdlemi2  39678  cdlemj1  39680  tendocan  39683  cdlemk5a  39694  cdlemki  39700  cdlemkvcl  39701  cdlemk10  39702  cdlemksv2  39706  cdlemkole  39712  cdlemk14  39713  cdlemk15  39714  cdlemk16a  39715  cdlemk16  39716  cdlemk17  39717  cdlemk18  39727  cdlemk19  39728  cdlemkoatnle-2N  39734  cdlemk13-2N  39735  cdlemkole-2N  39736  cdlemk14-2N  39737  cdlemk15-2N  39738  cdlemk16-2N  39739  cdlemk17-2N  39740  cdlemk18-2N  39745  cdlemk19-2N  39746  cdlemk30  39753  cdlemk18-3N  39759  cdlemk23-3  39761  cdlemk25-3  39763  cdlemk27-3  39766  cdlemk37  39773  cdlemkfid1N  39780  cdlemkid1  39781  cdlemky  39785  cdlemk11ta  39788  cdlemk47  39808  cdlemk48  39809  cdlemk49  39810  cdlemk50  39811  cdlemk51  39812  cdlemk52  39813  cdlemk53a  39814  cdlemk54  39817  cdlemk39u1  39826  cdlemk19u1  39828  cdleml1N  39835  cdleml2N  39836  cdleml3N  39837  dia2dimlem6  39928  cdlemn2  40054  cdlemn2a  40055  cdlemn5pre  40059  cdlemn10  40065  cdlemn11c  40068  cdlemn11pre  40069  dihjustlem  40075  dihjust  40076  lclkrlem2y  40390  relexpmulnn  42445  natglobalincr  45577  lincreslvec3  47116  iscnrm3llem1  47535  iscnrm3l  47537  amgmwlem  47802