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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp121  1305  simp221  1314  simp321  1323  omeulem1  8638  cofsmo  10338  axdc4lem  10524  0catg  17746  funcoppc  17939  funcres  17960  catcisolem  18177  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  mulgdirlem  19145  mdetunilem4  22642  mdetuni0  22648  mdetmul  22650  prdsxmetlem  24399  isosctrlem3  26881  isosctr  26882  amgmlem  27051  nosupbnd2lem1  27778  addsass  28056  f1otrg  28897  colinearalg  28943  ax5seglem6  28967  ax5seg  28971  axpasch  28974  axeuclidlem  28995  axeuclid  28996  uhgr2edg  29243  numclwlk1lem2  30402  ogrpsub  33066  ogrpaddlt  33067  ogrpsublt  33071  rhmdvd  33313  bnj1128  34966  mclspps  35552  cgrtr  35956  cgrtr3  35958  ofscom  35971  segconeq  35974  ifscgr  36008  btwnxfr  36020  colinearxfr  36039  lineext  36040  brofs2  36041  brifs2  36042  fscgr  36044  linecgr  36045  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem7  36057  seglecgr12im  36074  seglecgr12  36075  segletr  36078  broutsideof3  36090  outsideofeq  36094  lineunray  36111  lineelsb2  36112  linecom  36114  lshpkrlem5  39070  omlmod1i2N  39216  cvrnbtwn3  39232  cvrcmp  39239  cvrcmp2  39240  cvlexch2  39285  cvlexchb2  39287  cvlatexchb2  39291  cvlatexch2  39293  cvlatexch3  39294  cvlsupr7  39304  atnlej1  39336  atnlej2  39337  2llnneN  39366  cvratlem  39378  atcvrneN  39387  atcvrj1  39388  atlelt  39395  2atjm  39402  3noncolr2  39406  3noncolr1N  39407  3dimlem2  39416  3dim1  39424  3dim2  39425  1cvrat  39433  ps-1  39434  ps-2  39435  2atjlej  39436  hlatexch3N  39437  ps-2b  39439  3atlem1  39440  3atlem2  39441  3atlem5  39444  3atlem6  39445  llnle  39475  2atm  39484  ps-2c  39485  lplni2  39494  lplnle  39497  lplnnle2at  39498  lplnri3N  39512  llncvrlpln2  39514  2atmat  39518  2llnm2N  39525  2llnm4  39527  2llnmeqat  39528  lvolnle3at  39539  4atlem0ae  39551  4atlem0be  39552  4atlem3b  39555  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem12a  39567  4at2  39571  2lplnm2N  39578  lneq2at  39735  2llnma1b  39743  2llnma1  39744  2llnma3r  39745  2llnma2  39746  2llnma2rN  39747  cdlema1N  39748  paddasslem2  39778  paddasslem15  39791  paddasslem16  39792  pmodlem1  39803  pmodlem2  39804  pmod2iN  39806  hlmod1i  39813  atmod1i1m  39815  atmod2i1  39818  atmod2i2  39819  atmod3i1  39821  atmod3i2  39822  atmod4i1  39823  atmod4i2  39824  llnexchb2lem  39825  llnexch2N  39827  dalawlem3  39830  dalawlem4  39831  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem9  39836  dalawlem11  39838  dalawlem12  39839  dalawlem13  39840  dalawlem15  39842  osumcllem9N  39921  pl42lem1N  39936  4atexlems  40009  4atex2  40034  4atex2-0bOLDN  40036  trlval4  40145  cdlemc5  40152  cdlemc6  40153  cdlemd2  40156  cdlemd4  40158  cdlemd6  40160  cdleme00a  40166  cdleme0e  40174  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme4  40195  cdleme4a  40196  cdleme5  40197  cdleme9  40210  cdleme16aN  40216  cdleme11c  40218  cdleme11e  40220  cdleme11g  40222  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme11l  40226  cdleme11  40227  cdleme12  40228  cdleme14  40230  cdleme15c  40233  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme0nex  40247  cdleme18a  40248  cdleme18c  40250  cdleme18d  40252  cdlemednpq  40256  cdlemednuN  40257  cdleme20zN  40258  cdleme20y  40259  cdleme19a  40260  cdleme19b  40261  cdleme19d  40263  cdleme19e  40264  cdleme20aN  40266  cdleme20bN  40267  cdleme20c  40268  cdleme20d  40269  cdleme20f  40271  cdleme20g  40272  cdleme20i  40274  cdleme20j  40275  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21b  40283  cdleme21c  40284  cdleme21e  40288  cdleme21f  40289  cdleme22a  40297  cdleme22b  40298  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme26eALTN  40318  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme27N  40326  cdleme28a  40327  cdleme28b  40328  cdleme30a  40335  cdleme43fsv1snlem  40377  cdlemefs31fv1  40381  cdlemefs45eN  40388  cdleme32b  40399  cdleme32c  40400  cdleme32d  40401  cdleme35h  40413  cdleme36a  40417  cdleme36m  40418  cdleme37m  40419  cdleme40m  40424  cdleme40n  40425  cdleme41sn3aw  40431  cdleme41sn4aw  40432  cdleme41fva11  40434  cdleme42k  40441  cdleme43cN  40448  cdleme43dN  40449  cdleme46f2g1  40451  cdlemeg47rv2  40467  cdlemeg46sfg  40477  cdlemeg46fjgN  40478  cdlemeg46rjgN  40479  cdlemeg46fjv  40480  cdlemeg46frv  40482  cdlemeg46vrg  40484  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdlemg4a  40565  cdlemg4d  40570  cdlemg4e  40571  cdlemg4f  40572  cdlemg4g  40573  cdlemg4  40574  cdlemg6d  40578  cdlemg6e  40579  cdlemg8b  40585  cdlemg8c  40586  cdlemg9a  40589  cdlemg9b  40590  cdlemg10a  40597  cdlemg10  40598  cdlemg12a  40600  cdlemg12b  40601  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg17dN  40620  cdlemg17dALTN  40621  cdlemg17e  40622  cdlemg17f  40623  cdlemg17g  40624  cdlemg17h  40625  cdlemg17i  40626  cdlemg17pq  40629  cdlemg17iqN  40631  cdlemg17  40634  cdlemg18b  40636  cdlemg18c  40637  cdlemg19a  40640  cdlemg19  40641  cdlemg28a  40650  cdlemg27b  40653  cdlemg28b  40660  cdlemg28  40661  cdlemg33a  40663  cdlemg33b  40664  cdlemg33c  40665  cdlemg33d  40666  cdlemg33e  40667  cdlemg33  40668  cdlemg35  40670  cdlemg36  40671  cdlemg44a  40688  cdlemh  40774  cdlemi2  40776  cdlemj1  40778  tendocan  40781  cdlemk5a  40792  cdlemki  40798  cdlemkvcl  40799  cdlemk10  40800  cdlemksv2  40804  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk16a  40813  cdlemk16  40814  cdlemk17  40815  cdlemk18  40825  cdlemk19  40826  cdlemkoatnle-2N  40832  cdlemk13-2N  40833  cdlemkole-2N  40834  cdlemk14-2N  40835  cdlemk15-2N  40836  cdlemk16-2N  40837  cdlemk17-2N  40838  cdlemk18-2N  40843  cdlemk19-2N  40844  cdlemk30  40851  cdlemk18-3N  40857  cdlemk23-3  40859  cdlemk25-3  40861  cdlemk27-3  40864  cdlemk37  40871  cdlemkfid1N  40878  cdlemkid1  40879  cdlemky  40883  cdlemk11ta  40886  cdlemk47  40906  cdlemk48  40907  cdlemk49  40908  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk53a  40912  cdlemk54  40915  cdlemk39u1  40924  cdlemk19u1  40926  cdleml1N  40933  cdleml2N  40934  cdleml3N  40935  dia2dimlem6  41026  cdlemn2  41152  cdlemn2a  41153  cdlemn5pre  41157  cdlemn10  41163  cdlemn11c  41166  cdlemn11pre  41167  dihjustlem  41173  dihjust  41174  lclkrlem2y  41488  aks6d1c1  42073  relexpmulnn  43671  natglobalincr  46796  lincreslvec3  48211  iscnrm3llem1  48629  iscnrm3l  48631  amgmwlem  48896