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  8506  cofsmo  10171  axdc4lem  10357  0catg  17602  funcoppc  17790  funcres  17811  catcisolem  18025  1stfcl  18111  2ndfcl  18112  prfcl  18117  evlfcl  18136  curf1cl  18142  curfcl  18146  hofcl  18173  mulgdirlem  19026  ogrpsub  20057  ogrpaddlt  20058  ogrpsublt  20062  mdetunilem4  22550  mdetuni0  22556  mdetmul  22558  prdsxmetlem  24303  isosctrlem3  26777  isosctr  26778  amgmlem  26947  nosupbnd2lem1  27674  addsass  27968  f1otrg  28869  colinearalg  28909  ax5seglem6  28933  ax5seg  28937  axpasch  28940  axeuclidlem  28961  axeuclid  28962  uhgr2edg  29207  numclwlk1lem2  30371  rhmdvd  33333  bnj1128  35074  mclspps  35700  cgrtr  36108  cgrtr3  36110  ofscom  36123  segconeq  36126  ifscgr  36160  btwnxfr  36172  colinearxfr  36191  lineext  36192  brofs2  36193  brifs2  36194  fscgr  36196  linecgr  36197  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem3  36205  btwnconn1lem4  36206  btwnconn1lem5  36207  btwnconn1lem6  36208  btwnconn1lem7  36209  seglecgr12im  36226  seglecgr12  36227  segletr  36230  broutsideof3  36242  outsideofeq  36246  lineunray  36263  lineelsb2  36264  linecom  36266  lshpkrlem5  39286  omlmod1i2N  39432  cvrnbtwn3  39448  cvrcmp  39455  cvrcmp2  39456  cvlexch2  39501  cvlexchb2  39503  cvlatexchb2  39507  cvlatexch2  39509  cvlatexch3  39510  cvlsupr7  39520  atnlej1  39551  atnlej2  39552  2llnneN  39581  cvratlem  39593  atcvrneN  39602  atcvrj1  39603  atlelt  39610  2atjm  39617  3noncolr2  39621  3noncolr1N  39622  3dimlem2  39631  3dim1  39639  3dim2  39640  1cvrat  39648  ps-1  39649  ps-2  39650  2atjlej  39651  hlatexch3N  39652  ps-2b  39654  3atlem1  39655  3atlem2  39656  3atlem5  39659  3atlem6  39660  llnle  39690  2atm  39699  ps-2c  39700  lplni2  39709  lplnle  39712  lplnnle2at  39713  lplnri3N  39727  llncvrlpln2  39729  2atmat  39733  2llnm2N  39740  2llnm4  39742  2llnmeqat  39743  lvolnle3at  39754  4atlem0ae  39766  4atlem0be  39767  4atlem3b  39770  4atlem9  39775  4atlem10a  39776  4atlem10  39778  4atlem11a  39779  4atlem12a  39782  4at2  39786  2lplnm2N  39793  lneq2at  39950  2llnma1b  39958  2llnma1  39959  2llnma3r  39960  2llnma2  39961  2llnma2rN  39962  cdlema1N  39963  paddasslem2  39993  paddasslem15  40006  paddasslem16  40007  pmodlem1  40018  pmodlem2  40019  pmod2iN  40021  hlmod1i  40028  atmod1i1m  40030  atmod2i1  40033  atmod2i2  40034  atmod3i1  40036  atmod3i2  40037  atmod4i1  40038  atmod4i2  40039  llnexchb2lem  40040  llnexch2N  40042  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem13  40055  dalawlem15  40057  osumcllem9N  40136  pl42lem1N  40151  4atexlems  40224  4atex2  40249  4atex2-0bOLDN  40251  trlval4  40360  cdlemc5  40367  cdlemc6  40368  cdlemd2  40371  cdlemd4  40373  cdlemd6  40375  cdleme00a  40381  cdleme0e  40389  cdleme3g  40406  cdleme3h  40407  cdleme3  40409  cdleme4  40410  cdleme4a  40411  cdleme5  40412  cdleme9  40425  cdleme16aN  40431  cdleme11c  40433  cdleme11e  40435  cdleme11g  40437  cdleme11h  40438  cdleme11j  40439  cdleme11k  40440  cdleme11l  40441  cdleme11  40442  cdleme12  40443  cdleme14  40445  cdleme15c  40448  cdleme16b  40451  cdleme16c  40452  cdleme16d  40453  cdleme16e  40454  cdleme16f  40455  cdleme0nex  40462  cdleme18a  40463  cdleme18c  40465  cdleme18d  40467  cdlemednpq  40471  cdlemednuN  40472  cdleme20zN  40473  cdleme20y  40474  cdleme19a  40475  cdleme19b  40476  cdleme19d  40478  cdleme19e  40479  cdleme20aN  40481  cdleme20bN  40482  cdleme20c  40483  cdleme20d  40484  cdleme20f  40486  cdleme20g  40487  cdleme20i  40489  cdleme20j  40490  cdleme20l1  40492  cdleme20l2  40493  cdleme20l  40494  cdleme20m  40495  cdleme21b  40498  cdleme21c  40499  cdleme21e  40503  cdleme21f  40504  cdleme22a  40512  cdleme22b  40513  cdleme22e  40516  cdleme22eALTN  40517  cdleme22f  40518  cdleme26eALTN  40533  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme27N  40541  cdleme28a  40542  cdleme28b  40543  cdleme30a  40550  cdleme43fsv1snlem  40592  cdlemefs31fv1  40596  cdlemefs45eN  40603  cdleme32b  40614  cdleme32c  40615  cdleme32d  40616  cdleme35h  40628  cdleme36a  40632  cdleme36m  40633  cdleme37m  40634  cdleme40m  40639  cdleme40n  40640  cdleme41sn3aw  40646  cdleme41sn4aw  40647  cdleme41fva11  40649  cdleme42k  40656  cdleme43cN  40663  cdleme43dN  40664  cdleme46f2g1  40666  cdlemeg47rv2  40682  cdlemeg46sfg  40692  cdlemeg46fjgN  40693  cdlemeg46rjgN  40694  cdlemeg46fjv  40695  cdlemeg46frv  40697  cdlemeg46vrg  40699  cdlemeg46rgv  40700  cdlemeg46req  40701  cdlemeg46gfv  40702  cdlemg4a  40780  cdlemg4d  40785  cdlemg4e  40786  cdlemg4f  40787  cdlemg4g  40788  cdlemg4  40789  cdlemg6d  40793  cdlemg6e  40794  cdlemg8b  40800  cdlemg8c  40801  cdlemg9a  40804  cdlemg9b  40805  cdlemg10a  40812  cdlemg10  40813  cdlemg12a  40815  cdlemg12b  40816  cdlemg12f  40820  cdlemg12g  40821  cdlemg12  40822  cdlemg17dN  40835  cdlemg17dALTN  40836  cdlemg17e  40837  cdlemg17f  40838  cdlemg17g  40839  cdlemg17h  40840  cdlemg17i  40841  cdlemg17pq  40844  cdlemg17iqN  40846  cdlemg17  40849  cdlemg18b  40851  cdlemg18c  40852  cdlemg19a  40855  cdlemg19  40856  cdlemg28a  40865  cdlemg27b  40868  cdlemg28b  40875  cdlemg28  40876  cdlemg33a  40878  cdlemg33b  40879  cdlemg33c  40880  cdlemg33d  40881  cdlemg33e  40882  cdlemg33  40883  cdlemg35  40885  cdlemg36  40886  cdlemg44a  40903  cdlemh  40989  cdlemi2  40991  cdlemj1  40993  tendocan  40996  cdlemk5a  41007  cdlemki  41013  cdlemkvcl  41014  cdlemk10  41015  cdlemksv2  41019  cdlemkole  41025  cdlemk14  41026  cdlemk15  41027  cdlemk16a  41028  cdlemk16  41029  cdlemk17  41030  cdlemk18  41040  cdlemk19  41041  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk30  41066  cdlemk18-3N  41072  cdlemk23-3  41074  cdlemk25-3  41076  cdlemk27-3  41079  cdlemk37  41086  cdlemkfid1N  41093  cdlemkid1  41094  cdlemky  41098  cdlemk11ta  41101  cdlemk47  41121  cdlemk48  41122  cdlemk49  41123  cdlemk50  41124  cdlemk51  41125  cdlemk52  41126  cdlemk53a  41127  cdlemk54  41130  cdlemk39u1  41139  cdlemk19u1  41141  cdleml1N  41148  cdleml2N  41149  cdleml3N  41150  dia2dimlem6  41241  cdlemn2  41367  cdlemn2a  41368  cdlemn5pre  41372  cdlemn10  41378  cdlemn11c  41381  cdlemn11pre  41382  dihjustlem  41388  dihjust  41389  lclkrlem2y  41703  aks6d1c1  42282  relexpmulnn  43866  ormkglobd  47035  natglobalincr  47037  lincreslvec3  48644  iscnrm3llem1  49110  iscnrm3l  49112  swapffunc  49443  fucofunc  49520  amgmwlem  49963