Theorem simp21 1207

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 1137	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1135	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8582  cofsmo  10264  axdc4lem  10450  0catg  17632  funcoppc  17825  funcres  17846  catcisolem  18060  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  mulgdirlem  18985  mdetunilem4  22117  mdetuni0  22123  mdetmul  22125  prdsxmetlem  23874  isosctrlem3  26325  isosctr  26326  amgmlem  26494  nosupbnd2lem1  27218  addsass  27488  f1otrg  28122  colinearalg  28168  ax5seglem6  28192  ax5seg  28196  axpasch  28199  axeuclidlem  28220  axeuclid  28221  uhgr2edg  28465  numclwlk1lem2  29623  ogrpsub  32234  ogrpaddlt  32235  ogrpsublt  32239  rhmdvd  32436  bnj1128  34001  mclspps  34575  cgrtr  34964  cgrtr3  34966  ofscom  34979  segconeq  34982  ifscgr  35016  btwnxfr  35028  colinearxfr  35047  lineext  35048  brofs2  35049  brifs2  35050  fscgr  35052  linecgr  35053  btwnconn1lem1  35059  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem7  35065  seglecgr12im  35082  seglecgr12  35083  segletr  35086  broutsideof3  35098  outsideofeq  35102  lineunray  35119  lineelsb2  35120  linecom  35122  lshpkrlem5  37984  omlmod1i2N  38130  cvrnbtwn3  38146  cvrcmp  38153  cvrcmp2  38154  cvlexch2  38199  cvlexchb2  38201  cvlatexchb2  38205  cvlatexch2  38207  cvlatexch3  38208  cvlsupr7  38218  atnlej1  38250  atnlej2  38251  2llnneN  38280  cvratlem  38292  atcvrneN  38301  atcvrj1  38302  atlelt  38309  2atjm  38316  3noncolr2  38320  3noncolr1N  38321  3dimlem2  38330  3dim1  38338  3dim2  38339  1cvrat  38347  ps-1  38348  ps-2  38349  2atjlej  38350  hlatexch3N  38351  ps-2b  38353  3atlem1  38354  3atlem2  38355  3atlem5  38358  3atlem6  38359  llnle  38389  2atm  38398  ps-2c  38399  lplni2  38408  lplnle  38411  lplnnle2at  38412  lplnri3N  38426  llncvrlpln2  38428  2atmat  38432  2llnm2N  38439  2llnm4  38441  2llnmeqat  38442  lvolnle3at  38453  4atlem0ae  38465  4atlem0be  38466  4atlem3b  38469  4atlem9  38474  4atlem10a  38475  4atlem10  38477  4atlem11a  38478  4atlem12a  38481  4at2  38485  2lplnm2N  38492  lneq2at  38649  2llnma1b  38657  2llnma1  38658  2llnma3r  38659  2llnma2  38660  2llnma2rN  38661  cdlema1N  38662  paddasslem2  38692  paddasslem15  38705  paddasslem16  38706  pmodlem1  38717  pmodlem2  38718  pmod2iN  38720  hlmod1i  38727  atmod1i1m  38729  atmod2i1  38732  atmod2i2  38733  atmod3i1  38735  atmod3i2  38736  atmod4i1  38737  atmod4i2  38738  llnexchb2lem  38739  llnexch2N  38741  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem12  38753  dalawlem13  38754  dalawlem15  38756  osumcllem9N  38835  pl42lem1N  38850  4atexlems  38923  4atex2  38948  4atex2-0bOLDN  38950  trlval4  39059  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdlemd4  39072  cdlemd6  39074  cdleme00a  39080  cdleme0e  39088  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme5  39111  cdleme9  39124  cdleme16aN  39130  cdleme11c  39132  cdleme11e  39134  cdleme11g  39136  cdleme11h  39137  cdleme11j  39138  cdleme11k  39139  cdleme11l  39140  cdleme11  39141  cdleme12  39142  cdleme14  39144  cdleme15c  39147  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme16e  39153  cdleme16f  39154  cdleme0nex  39161  cdleme18a  39162  cdleme18c  39164  cdleme18d  39166  cdlemednpq  39170  cdlemednuN  39171  cdleme20zN  39172  cdleme20y  39173  cdleme19a  39174  cdleme19b  39175  cdleme19d  39177  cdleme19e  39178  cdleme20aN  39180  cdleme20bN  39181  cdleme20c  39182  cdleme20d  39183  cdleme20f  39185  cdleme20g  39186  cdleme20i  39188  cdleme20j  39189  cdleme20l1  39191  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21b  39197  cdleme21c  39198  cdleme21e  39202  cdleme21f  39203  cdleme22a  39211  cdleme22b  39212  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme26eALTN  39232  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme27N  39240  cdleme28a  39241  cdleme28b  39242  cdleme30a  39249  cdleme43fsv1snlem  39291  cdlemefs31fv1  39295  cdlemefs45eN  39302  cdleme32b  39313  cdleme32c  39314  cdleme32d  39315  cdleme35h  39327  cdleme36a  39331  cdleme36m  39332  cdleme37m  39333  cdleme40m  39338  cdleme40n  39339  cdleme41sn3aw  39345  cdleme41sn4aw  39346  cdleme41fva11  39348  cdleme42k  39355  cdleme43cN  39362  cdleme43dN  39363  cdleme46f2g1  39365  cdlemeg47rv2  39381  cdlemeg46sfg  39391  cdlemeg46fjgN  39392  cdlemeg46rjgN  39393  cdlemeg46fjv  39394  cdlemeg46frv  39396  cdlemeg46vrg  39398  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemeg46gfv  39401  cdlemg4a  39479  cdlemg4d  39484  cdlemg4e  39485  cdlemg4f  39486  cdlemg4g  39487  cdlemg4  39488  cdlemg6d  39492  cdlemg6e  39493  cdlemg8b  39499  cdlemg8c  39500  cdlemg9a  39503  cdlemg9b  39504  cdlemg10a  39511  cdlemg10  39512  cdlemg12a  39514  cdlemg12b  39515  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg17dN  39534  cdlemg17dALTN  39535  cdlemg17e  39536  cdlemg17f  39537  cdlemg17g  39538  cdlemg17h  39539  cdlemg17i  39540  cdlemg17pq  39543  cdlemg17iqN  39545  cdlemg17  39548  cdlemg18b  39550  cdlemg18c  39551  cdlemg19a  39554  cdlemg19  39555  cdlemg28a  39564  cdlemg27b  39567  cdlemg28b  39574  cdlemg28  39575  cdlemg33a  39577  cdlemg33b  39578  cdlemg33c  39579  cdlemg33d  39580  cdlemg33e  39581  cdlemg33  39582  cdlemg35  39584  cdlemg36  39585  cdlemg44a  39602  cdlemh  39688  cdlemi2  39690  cdlemj1  39692  tendocan  39695  cdlemk5a  39706  cdlemki  39712  cdlemkvcl  39713  cdlemk10  39714  cdlemksv2  39718  cdlemkole  39724  cdlemk14  39725  cdlemk15  39726  cdlemk16a  39727  cdlemk16  39728  cdlemk17  39729  cdlemk18  39739  cdlemk19  39740  cdlemkoatnle-2N  39746  cdlemk13-2N  39747  cdlemkole-2N  39748  cdlemk14-2N  39749  cdlemk15-2N  39750  cdlemk16-2N  39751  cdlemk17-2N  39752  cdlemk18-2N  39757  cdlemk19-2N  39758  cdlemk30  39765  cdlemk18-3N  39771  cdlemk23-3  39773  cdlemk25-3  39775  cdlemk27-3  39778  cdlemk37  39785  cdlemkfid1N  39792  cdlemkid1  39793  cdlemky  39797  cdlemk11ta  39800  cdlemk47  39820  cdlemk48  39821  cdlemk49  39822  cdlemk50  39823  cdlemk51  39824  cdlemk52  39825  cdlemk53a  39826  cdlemk54  39829  cdlemk39u1  39838  cdlemk19u1  39840  cdleml1N  39847  cdleml2N  39848  cdleml3N  39849  dia2dimlem6  39940  cdlemn2  40066  cdlemn2a  40067  cdlemn5pre  40071  cdlemn10  40077  cdlemn11c  40080  cdlemn11pre  40081  dihjustlem  40087  dihjust  40088  lclkrlem2y  40402  relexpmulnn  42460  natglobalincr  45591  lincreslvec3  47163  iscnrm3llem1  47582  iscnrm3l  47584  amgmwlem  47849