Theorem simp21 1225

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp121  1324  simp221  1333  simp321  1342  omeulem1  8569  cofsmo  10271  axdc4lem  10457  0catg  17776  funcoppc  17964  funcres  17985  catcisolem  18199  1stfcl  18285  2ndfcl  18286  prfcl  18291  evlfcl  18310  curf1cl  18316  curfcl  18320  hofcl  18347  mulgdirlem  19228  ogrpsub  20264  ogrpaddlt  20265  ogrpsublt  20269  mdetunilem4  22837  mdetuni0  22843  mdetmul  22845  prdsxmetlem  24594  isosctrlem3  27057  isosctr  27058  amgmlem  27226  nosupbnd2lem1  27951  addsass  28270  f1otrg  29327  colinearalg  29367  ax5seglem6  29391  ax5seg  29395  axpasch  29398  axeuclidlem  29419  axeuclid  29420  uhgr2edg  29668  numclwlk1lem2  30850  rhmdvd  33764  bnj1128  35499  mclspps  36163  cgrtr  36572  cgrtr3  36574  ofscom  36587  segconeq  36590  ifscgr  36624  btwnxfr  36636  colinearxfr  36655  lineext  36656  brofs2  36657  brifs2  36658  fscgr  36660  linecgr  36661  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem3  36669  btwnconn1lem4  36670  btwnconn1lem5  36671  btwnconn1lem6  36672  btwnconn1lem7  36673  seglecgr12im  36690  seglecgr12  36691  segletr  36694  broutsideof3  36706  outsideofeq  36710  lineunray  36727  lineelsb2  36728  linecom  36730  lshpkrlem5  39987  omlmod1i2N  40133  cvrnbtwn3  40149  cvrcmp  40156  cvrcmp2  40157  cvlexch2  40202  cvlexchb2  40204  cvlatexchb2  40208  cvlatexch2  40210  cvlatexch3  40211  cvlsupr7  40221  atnlej1  40252  atnlej2  40253  2llnneN  40282  cvratlem  40294  atcvrneN  40303  atcvrj1  40304  atlelt  40311  2atjm  40318  3noncolr2  40322  3noncolr1N  40323  3dimlem2  40332  3dim1  40340  3dim2  40341  1cvrat  40349  ps-1  40350  ps-2  40351  2atjlej  40352  hlatexch3N  40353  ps-2b  40355  3atlem1  40356  3atlem2  40357  3atlem5  40360  3atlem6  40361  llnle  40391  2atm  40400  ps-2c  40401  lplni2  40410  lplnle  40413  lplnnle2at  40414  lplnri3N  40428  llncvrlpln2  40430  2atmat  40434  2llnm2N  40441  2llnm4  40443  2llnmeqat  40444  lvolnle3at  40455  4atlem0ae  40467  4atlem0be  40468  4atlem3b  40471  4atlem9  40476  4atlem10a  40477  4atlem10  40479  4atlem11a  40480  4atlem12a  40483  4at2  40487  2lplnm2N  40494  lneq2at  40651  2llnma1b  40659  2llnma1  40660  2llnma3r  40661  2llnma2  40662  2llnma2rN  40663  cdlema1N  40664  paddasslem2  40694  paddasslem15  40707  paddasslem16  40708  pmodlem1  40719  pmodlem2  40720  pmod2iN  40722  hlmod1i  40729  atmod1i1m  40731  atmod2i1  40734  atmod2i2  40735  atmod3i1  40737  atmod3i2  40738  atmod4i1  40739  atmod4i2  40740  llnexchb2lem  40741  llnexch2N  40743  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem13  40756  dalawlem15  40758  osumcllem9N  40837  pl42lem1N  40852  4atexlems  40925  4atex2  40950  4atex2-0bOLDN  40952  trlval4  41061  cdlemc5  41068  cdlemc6  41069  cdlemd2  41072  cdlemd4  41074  cdlemd6  41076  cdleme00a  41082  cdleme0e  41090  cdleme3g  41107  cdleme3h  41108  cdleme3  41110  cdleme4  41111  cdleme4a  41112  cdleme5  41113  cdleme9  41126  cdleme16aN  41132  cdleme11c  41134  cdleme11e  41136  cdleme11g  41138  cdleme11h  41139  cdleme11j  41140  cdleme11k  41141  cdleme11l  41142  cdleme11  41143  cdleme12  41144  cdleme14  41146  cdleme15c  41149  cdleme16b  41152  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme0nex  41163  cdleme18a  41164  cdleme18c  41166  cdleme18d  41168  cdlemednpq  41172  cdlemednuN  41173  cdleme20zN  41174  cdleme20y  41175  cdleme19a  41176  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20aN  41182  cdleme20bN  41183  cdleme20c  41184  cdleme20d  41185  cdleme20f  41187  cdleme20g  41188  cdleme20i  41190  cdleme20j  41191  cdleme20l1  41193  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme21b  41199  cdleme21c  41200  cdleme21e  41204  cdleme21f  41205  cdleme22a  41213  cdleme22b  41214  cdleme22e  41217  cdleme22eALTN  41218  cdleme22f  41219  cdleme26eALTN  41234  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme27N  41242  cdleme28a  41243  cdleme28b  41244  cdleme30a  41251  cdleme43fsv1snlem  41293  cdlemefs31fv1  41297  cdlemefs45eN  41304  cdleme32b  41315  cdleme32c  41316  cdleme32d  41317  cdleme35h  41329  cdleme36a  41333  cdleme36m  41334  cdleme37m  41335  cdleme40m  41340  cdleme40n  41341  cdleme41sn3aw  41347  cdleme41sn4aw  41348  cdleme41fva11  41350  cdleme42k  41357  cdleme43cN  41364  cdleme43dN  41365  cdleme46f2g1  41367  cdlemeg47rv2  41383  cdlemeg46sfg  41393  cdlemeg46fjgN  41394  cdlemeg46rjgN  41395  cdlemeg46fjv  41396  cdlemeg46frv  41398  cdlemeg46vrg  41400  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemeg46gfv  41403  cdlemg4a  41481  cdlemg4d  41486  cdlemg4e  41487  cdlemg4f  41488  cdlemg4g  41489  cdlemg4  41490  cdlemg6d  41494  cdlemg6e  41495  cdlemg8b  41501  cdlemg8c  41502  cdlemg9a  41505  cdlemg9b  41506  cdlemg10a  41513  cdlemg10  41514  cdlemg12a  41516  cdlemg12b  41517  cdlemg12f  41521  cdlemg12g  41522  cdlemg12  41523  cdlemg17dN  41536  cdlemg17dALTN  41537  cdlemg17e  41538  cdlemg17f  41539  cdlemg17g  41540  cdlemg17h  41541  cdlemg17i  41542  cdlemg17pq  41545  cdlemg17iqN  41547  cdlemg17  41550  cdlemg18b  41552  cdlemg18c  41553  cdlemg19a  41556  cdlemg19  41557  cdlemg28a  41566  cdlemg27b  41569  cdlemg28b  41576  cdlemg28  41577  cdlemg33a  41579  cdlemg33b  41580  cdlemg33c  41581  cdlemg33d  41582  cdlemg33e  41583  cdlemg33  41584  cdlemg35  41586  cdlemg36  41587  cdlemg44a  41604  cdlemh  41690  cdlemi2  41692  cdlemj1  41694  tendocan  41697  cdlemk5a  41708  cdlemki  41714  cdlemkvcl  41715  cdlemk10  41716  cdlemksv2  41720  cdlemkole  41726  cdlemk14  41727  cdlemk15  41728  cdlemk16a  41729  cdlemk16  41730  cdlemk17  41731  cdlemk18  41741  cdlemk19  41742  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk30  41767  cdlemk18-3N  41773  cdlemk23-3  41775  cdlemk25-3  41777  cdlemk27-3  41780  cdlemk37  41787  cdlemkfid1N  41794  cdlemkid1  41795  cdlemky  41799  cdlemk11ta  41802  cdlemk47  41822  cdlemk48  41823  cdlemk49  41824  cdlemk50  41825  cdlemk51  41826  cdlemk52  41827  cdlemk53a  41828  cdlemk54  41831  cdlemk39u1  41840  cdlemk19u1  41842  cdleml1N  41849  cdleml2N  41850  cdleml3N  41851  dia2dimlem6  41942  cdlemn2  42068  cdlemn2a  42069  cdlemn5pre  42073  cdlemn10  42079  cdlemn11c  42082  cdlemn11pre  42083  dihjustlem  42089  dihjust  42090  lclkrlem2y  42404  aks6d1c1  42982  relexpmulnn  44549  ormkglobd  47705  lincreslvec3  49412  iscnrm3llem1  49875  iscnrm3l  49877  swapffunc  50208  fucofunc  50285  amgmwlem  50820