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  8523  cofsmo  10198  axdc4lem  10384  0catg  17625  funcoppc  17813  funcres  17834  catcisolem  18048  1stfcl  18134  2ndfcl  18135  prfcl  18140  evlfcl  18159  curf1cl  18165  curfcl  18169  hofcl  18196  mulgdirlem  19013  mdetunilem4  22478  mdetuni0  22484  mdetmul  22486  prdsxmetlem  24232  isosctrlem3  26706  isosctr  26707  amgmlem  26876  nosupbnd2lem1  27603  addsass  27888  f1otrg  28774  colinearalg  28813  ax5seglem6  28837  ax5seg  28841  axpasch  28844  axeuclidlem  28865  axeuclid  28866  uhgr2edg  29111  numclwlk1lem2  30272  ogrpsub  33003  ogrpaddlt  33004  ogrpsublt  33008  rhmdvd  33269  bnj1128  34953  mclspps  35544  cgrtr  35953  cgrtr3  35955  ofscom  35968  segconeq  35971  ifscgr  36005  btwnxfr  36017  colinearxfr  36036  lineext  36037  brofs2  36038  brifs2  36039  fscgr  36041  linecgr  36042  btwnconn1lem1  36048  btwnconn1lem2  36049  btwnconn1lem3  36050  btwnconn1lem4  36051  btwnconn1lem5  36052  btwnconn1lem6  36053  btwnconn1lem7  36054  seglecgr12im  36071  seglecgr12  36072  segletr  36075  broutsideof3  36087  outsideofeq  36091  lineunray  36108  lineelsb2  36109  linecom  36111  lshpkrlem5  39080  omlmod1i2N  39226  cvrnbtwn3  39242  cvrcmp  39249  cvrcmp2  39250  cvlexch2  39295  cvlexchb2  39297  cvlatexchb2  39301  cvlatexch2  39303  cvlatexch3  39304  cvlsupr7  39314  atnlej1  39346  atnlej2  39347  2llnneN  39376  cvratlem  39388  atcvrneN  39397  atcvrj1  39398  atlelt  39405  2atjm  39412  3noncolr2  39416  3noncolr1N  39417  3dimlem2  39426  3dim1  39434  3dim2  39435  1cvrat  39443  ps-1  39444  ps-2  39445  2atjlej  39446  hlatexch3N  39447  ps-2b  39449  3atlem1  39450  3atlem2  39451  3atlem5  39454  3atlem6  39455  llnle  39485  2atm  39494  ps-2c  39495  lplni2  39504  lplnle  39507  lplnnle2at  39508  lplnri3N  39522  llncvrlpln2  39524  2atmat  39528  2llnm2N  39535  2llnm4  39537  2llnmeqat  39538  lvolnle3at  39549  4atlem0ae  39561  4atlem0be  39562  4atlem3b  39565  4atlem9  39570  4atlem10a  39571  4atlem10  39573  4atlem11a  39574  4atlem12a  39577  4at2  39581  2lplnm2N  39588  lneq2at  39745  2llnma1b  39753  2llnma1  39754  2llnma3r  39755  2llnma2  39756  2llnma2rN  39757  cdlema1N  39758  paddasslem2  39788  paddasslem15  39801  paddasslem16  39802  pmodlem1  39813  pmodlem2  39814  pmod2iN  39816  hlmod1i  39823  atmod1i1m  39825  atmod2i1  39828  atmod2i2  39829  atmod3i1  39831  atmod3i2  39832  atmod4i1  39833  atmod4i2  39834  llnexchb2lem  39835  llnexch2N  39837  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem13  39850  dalawlem15  39852  osumcllem9N  39931  pl42lem1N  39946  4atexlems  40019  4atex2  40044  4atex2-0bOLDN  40046  trlval4  40155  cdlemc5  40162  cdlemc6  40163  cdlemd2  40166  cdlemd4  40168  cdlemd6  40170  cdleme00a  40176  cdleme0e  40184  cdleme3g  40201  cdleme3h  40202  cdleme3  40204  cdleme4  40205  cdleme4a  40206  cdleme5  40207  cdleme9  40220  cdleme16aN  40226  cdleme11c  40228  cdleme11e  40230  cdleme11g  40232  cdleme11h  40233  cdleme11j  40234  cdleme11k  40235  cdleme11l  40236  cdleme11  40237  cdleme12  40238  cdleme14  40240  cdleme15c  40243  cdleme16b  40246  cdleme16c  40247  cdleme16d  40248  cdleme16e  40249  cdleme16f  40250  cdleme0nex  40257  cdleme18a  40258  cdleme18c  40260  cdleme18d  40262  cdlemednpq  40266  cdlemednuN  40267  cdleme20zN  40268  cdleme20y  40269  cdleme19a  40270  cdleme19b  40271  cdleme19d  40273  cdleme19e  40274  cdleme20aN  40276  cdleme20bN  40277  cdleme20c  40278  cdleme20d  40279  cdleme20f  40281  cdleme20g  40282  cdleme20i  40284  cdleme20j  40285  cdleme20l1  40287  cdleme20l2  40288  cdleme20l  40289  cdleme20m  40290  cdleme21b  40293  cdleme21c  40294  cdleme21e  40298  cdleme21f  40299  cdleme22a  40307  cdleme22b  40308  cdleme22e  40311  cdleme22eALTN  40312  cdleme22f  40313  cdleme26eALTN  40328  cdleme26fALTN  40329  cdleme26f  40330  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme27N  40336  cdleme28a  40337  cdleme28b  40338  cdleme30a  40345  cdleme43fsv1snlem  40387  cdlemefs31fv1  40391  cdlemefs45eN  40398  cdleme32b  40409  cdleme32c  40410  cdleme32d  40411  cdleme35h  40423  cdleme36a  40427  cdleme36m  40428  cdleme37m  40429  cdleme40m  40434  cdleme40n  40435  cdleme41sn3aw  40441  cdleme41sn4aw  40442  cdleme41fva11  40444  cdleme42k  40451  cdleme43cN  40458  cdleme43dN  40459  cdleme46f2g1  40461  cdlemeg47rv2  40477  cdlemeg46sfg  40487  cdlemeg46fjgN  40488  cdlemeg46rjgN  40489  cdlemeg46fjv  40490  cdlemeg46frv  40492  cdlemeg46vrg  40494  cdlemeg46rgv  40495  cdlemeg46req  40496  cdlemeg46gfv  40497  cdlemg4a  40575  cdlemg4d  40580  cdlemg4e  40581  cdlemg4f  40582  cdlemg4g  40583  cdlemg4  40584  cdlemg6d  40588  cdlemg6e  40589  cdlemg8b  40595  cdlemg8c  40596  cdlemg9a  40599  cdlemg9b  40600  cdlemg10a  40607  cdlemg10  40608  cdlemg12a  40610  cdlemg12b  40611  cdlemg12f  40615  cdlemg12g  40616  cdlemg12  40617  cdlemg17dN  40630  cdlemg17dALTN  40631  cdlemg17e  40632  cdlemg17f  40633  cdlemg17g  40634  cdlemg17h  40635  cdlemg17i  40636  cdlemg17pq  40639  cdlemg17iqN  40641  cdlemg17  40644  cdlemg18b  40646  cdlemg18c  40647  cdlemg19a  40650  cdlemg19  40651  cdlemg28a  40660  cdlemg27b  40663  cdlemg28b  40670  cdlemg28  40671  cdlemg33a  40673  cdlemg33b  40674  cdlemg33c  40675  cdlemg33d  40676  cdlemg33e  40677  cdlemg33  40678  cdlemg35  40680  cdlemg36  40681  cdlemg44a  40698  cdlemh  40784  cdlemi2  40786  cdlemj1  40788  tendocan  40791  cdlemk5a  40802  cdlemki  40808  cdlemkvcl  40809  cdlemk10  40810  cdlemksv2  40814  cdlemkole  40820  cdlemk14  40821  cdlemk15  40822  cdlemk16a  40823  cdlemk16  40824  cdlemk17  40825  cdlemk18  40835  cdlemk19  40836  cdlemkoatnle-2N  40842  cdlemk13-2N  40843  cdlemkole-2N  40844  cdlemk14-2N  40845  cdlemk15-2N  40846  cdlemk16-2N  40847  cdlemk17-2N  40848  cdlemk18-2N  40853  cdlemk19-2N  40854  cdlemk30  40861  cdlemk18-3N  40867  cdlemk23-3  40869  cdlemk25-3  40871  cdlemk27-3  40874  cdlemk37  40881  cdlemkfid1N  40888  cdlemkid1  40889  cdlemky  40893  cdlemk11ta  40896  cdlemk47  40916  cdlemk48  40917  cdlemk49  40918  cdlemk50  40919  cdlemk51  40920  cdlemk52  40921  cdlemk53a  40922  cdlemk54  40925  cdlemk39u1  40934  cdlemk19u1  40936  cdleml1N  40943  cdleml2N  40944  cdleml3N  40945  dia2dimlem6  41036  cdlemn2  41162  cdlemn2a  41163  cdlemn5pre  41167  cdlemn10  41173  cdlemn11c  41176  cdlemn11pre  41177  dihjustlem  41183  dihjust  41184  lclkrlem2y  41498  aks6d1c1  42077  relexpmulnn  43671  ormkglobd  46846  natglobalincr  46848  lincreslvec3  48444  iscnrm3llem1  48910  iscnrm3l  48912  swapffunc  49244  fucofunc  49321  amgmwlem  49764