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  8509  cofsmo  10179  axdc4lem  10365  0catg  17611  funcoppc  17799  funcres  17820  catcisolem  18034  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlfcl  18145  curf1cl  18151  curfcl  18155  hofcl  18182  mulgdirlem  19035  ogrpsub  20066  ogrpaddlt  20067  ogrpsublt  20071  mdetunilem4  22559  mdetuni0  22565  mdetmul  22567  prdsxmetlem  24312  isosctrlem3  26786  isosctr  26787  amgmlem  26956  nosupbnd2lem1  27683  addsass  28001  f1otrg  28943  colinearalg  28983  ax5seglem6  29007  ax5seg  29011  axpasch  29014  axeuclidlem  29035  axeuclid  29036  uhgr2edg  29281  numclwlk1lem2  30445  rhmdvd  33405  bnj1128  35146  mclspps  35778  cgrtr  36186  cgrtr3  36188  ofscom  36201  segconeq  36204  ifscgr  36238  btwnxfr  36250  colinearxfr  36269  lineext  36270  brofs2  36271  brifs2  36272  fscgr  36274  linecgr  36275  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  seglecgr12im  36304  seglecgr12  36305  segletr  36308  broutsideof3  36320  outsideofeq  36324  lineunray  36341  lineelsb2  36342  linecom  36344  lshpkrlem5  39374  omlmod1i2N  39520  cvrnbtwn3  39536  cvrcmp  39543  cvrcmp2  39544  cvlexch2  39589  cvlexchb2  39591  cvlatexchb2  39595  cvlatexch2  39597  cvlatexch3  39598  cvlsupr7  39608  atnlej1  39639  atnlej2  39640  2llnneN  39669  cvratlem  39681  atcvrneN  39690  atcvrj1  39691  atlelt  39698  2atjm  39705  3noncolr2  39709  3noncolr1N  39710  3dimlem2  39719  3dim1  39727  3dim2  39728  1cvrat  39736  ps-1  39737  ps-2  39738  2atjlej  39739  hlatexch3N  39740  ps-2b  39742  3atlem1  39743  3atlem2  39744  3atlem5  39747  3atlem6  39748  llnle  39778  2atm  39787  ps-2c  39788  lplni2  39797  lplnle  39800  lplnnle2at  39801  lplnri3N  39815  llncvrlpln2  39817  2atmat  39821  2llnm2N  39828  2llnm4  39830  2llnmeqat  39831  lvolnle3at  39842  4atlem0ae  39854  4atlem0be  39855  4atlem3b  39858  4atlem9  39863  4atlem10a  39864  4atlem10  39866  4atlem11a  39867  4atlem12a  39870  4at2  39874  2lplnm2N  39881  lneq2at  40038  2llnma1b  40046  2llnma1  40047  2llnma3r  40048  2llnma2  40049  2llnma2rN  40050  cdlema1N  40051  paddasslem2  40081  paddasslem15  40094  paddasslem16  40095  pmodlem1  40106  pmodlem2  40107  pmod2iN  40109  hlmod1i  40116  atmod1i1m  40118  atmod2i1  40121  atmod2i2  40122  atmod3i1  40124  atmod3i2  40125  atmod4i1  40126  atmod4i2  40127  llnexchb2lem  40128  llnexch2N  40130  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem11  40141  dalawlem12  40142  dalawlem13  40143  dalawlem15  40145  osumcllem9N  40224  pl42lem1N  40239  4atexlems  40312  4atex2  40337  4atex2-0bOLDN  40339  trlval4  40448  cdlemc5  40455  cdlemc6  40456  cdlemd2  40459  cdlemd4  40461  cdlemd6  40463  cdleme00a  40469  cdleme0e  40477  cdleme3g  40494  cdleme3h  40495  cdleme3  40497  cdleme4  40498  cdleme4a  40499  cdleme5  40500  cdleme9  40513  cdleme16aN  40519  cdleme11c  40521  cdleme11e  40523  cdleme11g  40525  cdleme11h  40526  cdleme11j  40527  cdleme11k  40528  cdleme11l  40529  cdleme11  40530  cdleme12  40531  cdleme14  40533  cdleme15c  40536  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme0nex  40550  cdleme18a  40551  cdleme18c  40553  cdleme18d  40555  cdlemednpq  40559  cdlemednuN  40560  cdleme20zN  40561  cdleme20y  40562  cdleme19a  40563  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20aN  40569  cdleme20bN  40570  cdleme20c  40571  cdleme20d  40572  cdleme20f  40574  cdleme20g  40575  cdleme20i  40577  cdleme20j  40578  cdleme20l1  40580  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme21b  40586  cdleme21c  40587  cdleme21e  40591  cdleme21f  40592  cdleme22a  40600  cdleme22b  40601  cdleme22e  40604  cdleme22eALTN  40605  cdleme22f  40606  cdleme26eALTN  40621  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme27N  40629  cdleme28a  40630  cdleme28b  40631  cdleme30a  40638  cdleme43fsv1snlem  40680  cdlemefs31fv1  40684  cdlemefs45eN  40691  cdleme32b  40702  cdleme32c  40703  cdleme32d  40704  cdleme35h  40716  cdleme36a  40720  cdleme36m  40721  cdleme37m  40722  cdleme40m  40727  cdleme40n  40728  cdleme41sn3aw  40734  cdleme41sn4aw  40735  cdleme41fva11  40737  cdleme42k  40744  cdleme43cN  40751  cdleme43dN  40752  cdleme46f2g1  40754  cdlemeg47rv2  40770  cdlemeg46sfg  40780  cdlemeg46fjgN  40781  cdlemeg46rjgN  40782  cdlemeg46fjv  40783  cdlemeg46frv  40785  cdlemeg46vrg  40787  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemeg46gfv  40790  cdlemg4a  40868  cdlemg4d  40873  cdlemg4e  40874  cdlemg4f  40875  cdlemg4g  40876  cdlemg4  40877  cdlemg6d  40881  cdlemg6e  40882  cdlemg8b  40888  cdlemg8c  40889  cdlemg9a  40892  cdlemg9b  40893  cdlemg10a  40900  cdlemg10  40901  cdlemg12a  40903  cdlemg12b  40904  cdlemg12f  40908  cdlemg12g  40909  cdlemg12  40910  cdlemg17dN  40923  cdlemg17dALTN  40924  cdlemg17e  40925  cdlemg17f  40926  cdlemg17g  40927  cdlemg17h  40928  cdlemg17i  40929  cdlemg17pq  40932  cdlemg17iqN  40934  cdlemg17  40937  cdlemg18b  40939  cdlemg18c  40940  cdlemg19a  40943  cdlemg19  40944  cdlemg28a  40953  cdlemg27b  40956  cdlemg28b  40963  cdlemg28  40964  cdlemg33a  40966  cdlemg33b  40967  cdlemg33c  40968  cdlemg33d  40969  cdlemg33e  40970  cdlemg33  40971  cdlemg35  40973  cdlemg36  40974  cdlemg44a  40991  cdlemh  41077  cdlemi2  41079  cdlemj1  41081  tendocan  41084  cdlemk5a  41095  cdlemki  41101  cdlemkvcl  41102  cdlemk10  41103  cdlemksv2  41107  cdlemkole  41113  cdlemk14  41114  cdlemk15  41115  cdlemk16a  41116  cdlemk16  41117  cdlemk17  41118  cdlemk18  41128  cdlemk19  41129  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk30  41154  cdlemk18-3N  41160  cdlemk23-3  41162  cdlemk25-3  41164  cdlemk27-3  41167  cdlemk37  41174  cdlemkfid1N  41181  cdlemkid1  41182  cdlemky  41186  cdlemk11ta  41189  cdlemk47  41209  cdlemk48  41210  cdlemk49  41211  cdlemk50  41212  cdlemk51  41213  cdlemk52  41214  cdlemk53a  41215  cdlemk54  41218  cdlemk39u1  41227  cdlemk19u1  41229  cdleml1N  41236  cdleml2N  41237  cdleml3N  41238  dia2dimlem6  41329  cdlemn2  41455  cdlemn2a  41456  cdlemn5pre  41460  cdlemn10  41466  cdlemn11c  41469  cdlemn11pre  41470  dihjustlem  41476  dihjust  41477  lclkrlem2y  41791  aks6d1c1  42370  relexpmulnn  43950  ormkglobd  47119  natglobalincr  47121  lincreslvec3  48728  iscnrm3llem1  49194  iscnrm3l  49196  swapffunc  49527  fucofunc  49604  amgmwlem  50047