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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8592  cofsmo  10281  axdc4lem  10467  0catg  17698  funcoppc  17886  funcres  17907  catcisolem  18121  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlfcl  18232  curf1cl  18238  curfcl  18242  hofcl  18269  mulgdirlem  19086  mdetunilem4  22551  mdetuni0  22557  mdetmul  22559  prdsxmetlem  24305  isosctrlem3  26780  isosctr  26781  amgmlem  26950  nosupbnd2lem1  27677  addsass  27955  f1otrg  28796  colinearalg  28835  ax5seglem6  28859  ax5seg  28863  axpasch  28866  axeuclidlem  28887  axeuclid  28888  uhgr2edg  29133  numclwlk1lem2  30297  ogrpsub  33030  ogrpaddlt  33031  ogrpsublt  33035  rhmdvd  33286  bnj1128  34967  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  39078  omlmod1i2N  39224  cvrnbtwn3  39240  cvrcmp  39247  cvrcmp2  39248  cvlexch2  39293  cvlexchb2  39295  cvlatexchb2  39299  cvlatexch2  39301  cvlatexch3  39302  cvlsupr7  39312  atnlej1  39344  atnlej2  39345  2llnneN  39374  cvratlem  39386  atcvrneN  39395  atcvrj1  39396  atlelt  39403  2atjm  39410  3noncolr2  39414  3noncolr1N  39415  3dimlem2  39424  3dim1  39432  3dim2  39433  1cvrat  39441  ps-1  39442  ps-2  39443  2atjlej  39444  hlatexch3N  39445  ps-2b  39447  3atlem1  39448  3atlem2  39449  3atlem5  39452  3atlem6  39453  llnle  39483  2atm  39492  ps-2c  39493  lplni2  39502  lplnle  39505  lplnnle2at  39506  lplnri3N  39520  llncvrlpln2  39522  2atmat  39526  2llnm2N  39533  2llnm4  39535  2llnmeqat  39536  lvolnle3at  39547  4atlem0ae  39559  4atlem0be  39560  4atlem3b  39563  4atlem9  39568  4atlem10a  39569  4atlem10  39571  4atlem11a  39572  4atlem12a  39575  4at2  39579  2lplnm2N  39586  lneq2at  39743  2llnma1b  39751  2llnma1  39752  2llnma3r  39753  2llnma2  39754  2llnma2rN  39755  cdlema1N  39756  paddasslem2  39786  paddasslem15  39799  paddasslem16  39800  pmodlem1  39811  pmodlem2  39812  pmod2iN  39814  hlmod1i  39821  atmod1i1m  39823  atmod2i1  39826  atmod2i2  39827  atmod3i1  39829  atmod3i2  39830  atmod4i1  39831  atmod4i2  39832  llnexchb2lem  39833  llnexch2N  39835  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem13  39848  dalawlem15  39850  osumcllem9N  39929  pl42lem1N  39944  4atexlems  40017  4atex2  40042  4atex2-0bOLDN  40044  trlval4  40153  cdlemc5  40160  cdlemc6  40161  cdlemd2  40164  cdlemd4  40166  cdlemd6  40168  cdleme00a  40174  cdleme0e  40182  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme4  40203  cdleme4a  40204  cdleme5  40205  cdleme9  40218  cdleme16aN  40224  cdleme11c  40226  cdleme11e  40228  cdleme11g  40230  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme11l  40234  cdleme11  40235  cdleme12  40236  cdleme14  40238  cdleme15c  40241  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme0nex  40255  cdleme18a  40256  cdleme18c  40258  cdleme18d  40260  cdlemednpq  40264  cdlemednuN  40265  cdleme20zN  40266  cdleme20y  40267  cdleme19a  40268  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20aN  40274  cdleme20bN  40275  cdleme20c  40276  cdleme20d  40277  cdleme20f  40279  cdleme20g  40280  cdleme20i  40282  cdleme20j  40283  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21b  40291  cdleme21c  40292  cdleme21e  40296  cdleme21f  40297  cdleme22a  40305  cdleme22b  40306  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme26eALTN  40326  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme27N  40334  cdleme28a  40335  cdleme28b  40336  cdleme30a  40343  cdleme43fsv1snlem  40385  cdlemefs31fv1  40389  cdlemefs45eN  40396  cdleme32b  40407  cdleme32c  40408  cdleme32d  40409  cdleme35h  40421  cdleme36a  40425  cdleme36m  40426  cdleme37m  40427  cdleme40m  40432  cdleme40n  40433  cdleme41sn3aw  40439  cdleme41sn4aw  40440  cdleme41fva11  40442  cdleme42k  40449  cdleme43cN  40456  cdleme43dN  40457  cdleme46f2g1  40459  cdlemeg47rv2  40475  cdlemeg46sfg  40485  cdlemeg46fjgN  40486  cdlemeg46rjgN  40487  cdlemeg46fjv  40488  cdlemeg46frv  40490  cdlemeg46vrg  40492  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdlemg4a  40573  cdlemg4d  40578  cdlemg4e  40579  cdlemg4f  40580  cdlemg4g  40581  cdlemg4  40582  cdlemg6d  40586  cdlemg6e  40587  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg9b  40598  cdlemg10a  40605  cdlemg10  40606  cdlemg12a  40608  cdlemg12b  40609  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg17dN  40628  cdlemg17dALTN  40629  cdlemg17e  40630  cdlemg17f  40631  cdlemg17g  40632  cdlemg17h  40633  cdlemg17i  40634  cdlemg17pq  40637  cdlemg17iqN  40639  cdlemg17  40642  cdlemg18b  40644  cdlemg18c  40645  cdlemg19a  40648  cdlemg19  40649  cdlemg28a  40658  cdlemg27b  40661  cdlemg28b  40668  cdlemg28  40669  cdlemg33a  40671  cdlemg33b  40672  cdlemg33c  40673  cdlemg33d  40674  cdlemg33e  40675  cdlemg33  40676  cdlemg35  40678  cdlemg36  40679  cdlemg44a  40696  cdlemh  40782  cdlemi2  40784  cdlemj1  40786  tendocan  40789  cdlemk5a  40800  cdlemki  40806  cdlemkvcl  40807  cdlemk10  40808  cdlemksv2  40812  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  cdlemk17  40823  cdlemk18  40833  cdlemk19  40834  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk30  40859  cdlemk18-3N  40865  cdlemk23-3  40867  cdlemk25-3  40869  cdlemk27-3  40872  cdlemk37  40879  cdlemkfid1N  40886  cdlemkid1  40887  cdlemky  40891  cdlemk11ta  40894  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk54  40923  cdlemk39u1  40932  cdlemk19u1  40934  cdleml1N  40941  cdleml2N  40942  cdleml3N  40943  dia2dimlem6  41034  cdlemn2  41160  cdlemn2a  41161  cdlemn5pre  41165  cdlemn10  41171  cdlemn11c  41174  cdlemn11pre  41175  dihjustlem  41181  dihjust  41182  lclkrlem2y  41496  aks6d1c1  42075  relexpmulnn  43680  ormkglobd  46852  natglobalincr  46854  lincreslvec3  48406  iscnrm3llem1  48871  iscnrm3l  48873  swapffunc  49147  fucofunc  49218  amgmwlem  49614