Theorem simp21 1208

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp121  1307  simp221  1316  simp321  1325  omeulem1  8519  cofsmo  10191  axdc4lem  10377  0catg  17623  funcoppc  17811  funcres  17832  catcisolem  18046  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  mulgdirlem  19047  ogrpsub  20078  ogrpaddlt  20079  ogrpsublt  20083  mdetunilem4  22571  mdetuni0  22577  mdetmul  22579  prdsxmetlem  24324  isosctrlem3  26798  isosctr  26799  amgmlem  26968  nosupbnd2lem1  27695  addsass  28013  f1otrg  28955  colinearalg  28995  ax5seglem6  29019  ax5seg  29023  axpasch  29026  axeuclidlem  29047  axeuclid  29048  uhgr2edg  29293  numclwlk1lem2  30457  rhmdvd  33416  bnj1128  35165  mclspps  35797  cgrtr  36205  cgrtr3  36207  ofscom  36220  segconeq  36223  ifscgr  36257  btwnxfr  36269  colinearxfr  36288  lineext  36289  brofs2  36290  brifs2  36291  fscgr  36293  linecgr  36294  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  seglecgr12im  36323  seglecgr12  36324  segletr  36327  broutsideof3  36339  outsideofeq  36343  lineunray  36360  lineelsb2  36361  linecom  36363  lshpkrlem5  39487  omlmod1i2N  39633  cvrnbtwn3  39649  cvrcmp  39656  cvrcmp2  39657  cvlexch2  39702  cvlexchb2  39704  cvlatexchb2  39708  cvlatexch2  39710  cvlatexch3  39711  cvlsupr7  39721  atnlej1  39752  atnlej2  39753  2llnneN  39782  cvratlem  39794  atcvrneN  39803  atcvrj1  39804  atlelt  39811  2atjm  39818  3noncolr2  39822  3noncolr1N  39823  3dimlem2  39832  3dim1  39840  3dim2  39841  1cvrat  39849  ps-1  39850  ps-2  39851  2atjlej  39852  hlatexch3N  39853  ps-2b  39855  3atlem1  39856  3atlem2  39857  3atlem5  39860  3atlem6  39861  llnle  39891  2atm  39900  ps-2c  39901  lplni2  39910  lplnle  39913  lplnnle2at  39914  lplnri3N  39928  llncvrlpln2  39930  2atmat  39934  2llnm2N  39941  2llnm4  39943  2llnmeqat  39944  lvolnle3at  39955  4atlem0ae  39967  4atlem0be  39968  4atlem3b  39971  4atlem9  39976  4atlem10a  39977  4atlem10  39979  4atlem11a  39980  4atlem12a  39983  4at2  39987  2lplnm2N  39994  lneq2at  40151  2llnma1b  40159  2llnma1  40160  2llnma3r  40161  2llnma2  40162  2llnma2rN  40163  cdlema1N  40164  paddasslem2  40194  paddasslem15  40207  paddasslem16  40208  pmodlem1  40219  pmodlem2  40220  pmod2iN  40222  hlmod1i  40229  atmod1i1m  40231  atmod2i1  40234  atmod2i2  40235  atmod3i1  40237  atmod3i2  40238  atmod4i1  40239  atmod4i2  40240  llnexchb2lem  40241  llnexch2N  40243  dalawlem3  40246  dalawlem4  40247  dalawlem5  40248  dalawlem6  40249  dalawlem7  40250  dalawlem8  40251  dalawlem9  40252  dalawlem11  40254  dalawlem12  40255  dalawlem13  40256  dalawlem15  40258  osumcllem9N  40337  pl42lem1N  40352  4atexlems  40425  4atex2  40450  4atex2-0bOLDN  40452  trlval4  40561  cdlemc5  40568  cdlemc6  40569  cdlemd2  40572  cdlemd4  40574  cdlemd6  40576  cdleme00a  40582  cdleme0e  40590  cdleme3g  40607  cdleme3h  40608  cdleme3  40610  cdleme4  40611  cdleme4a  40612  cdleme5  40613  cdleme9  40626  cdleme16aN  40632  cdleme11c  40634  cdleme11e  40636  cdleme11g  40638  cdleme11h  40639  cdleme11j  40640  cdleme11k  40641  cdleme11l  40642  cdleme11  40643  cdleme12  40644  cdleme14  40646  cdleme15c  40649  cdleme16b  40652  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme16f  40656  cdleme0nex  40663  cdleme18a  40664  cdleme18c  40666  cdleme18d  40668  cdlemednpq  40672  cdlemednuN  40673  cdleme20zN  40674  cdleme20y  40675  cdleme19a  40676  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20aN  40682  cdleme20bN  40683  cdleme20c  40684  cdleme20d  40685  cdleme20f  40687  cdleme20g  40688  cdleme20i  40690  cdleme20j  40691  cdleme20l1  40693  cdleme20l2  40694  cdleme20l  40695  cdleme20m  40696  cdleme21b  40699  cdleme21c  40700  cdleme21e  40704  cdleme21f  40705  cdleme22a  40713  cdleme22b  40714  cdleme22e  40717  cdleme22eALTN  40718  cdleme22f  40719  cdleme26eALTN  40734  cdleme26fALTN  40735  cdleme26f  40736  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme27N  40742  cdleme28a  40743  cdleme28b  40744  cdleme30a  40751  cdleme43fsv1snlem  40793  cdlemefs31fv1  40797  cdlemefs45eN  40804  cdleme32b  40815  cdleme32c  40816  cdleme32d  40817  cdleme35h  40829  cdleme36a  40833  cdleme36m  40834  cdleme37m  40835  cdleme40m  40840  cdleme40n  40841  cdleme41sn3aw  40847  cdleme41sn4aw  40848  cdleme41fva11  40850  cdleme42k  40857  cdleme43cN  40864  cdleme43dN  40865  cdleme46f2g1  40867  cdlemeg47rv2  40883  cdlemeg46sfg  40893  cdlemeg46fjgN  40894  cdlemeg46rjgN  40895  cdlemeg46fjv  40896  cdlemeg46frv  40898  cdlemeg46vrg  40900  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemeg46gfv  40903  cdlemg4a  40981  cdlemg4d  40986  cdlemg4e  40987  cdlemg4f  40988  cdlemg4g  40989  cdlemg4  40990  cdlemg6d  40994  cdlemg6e  40995  cdlemg8b  41001  cdlemg8c  41002  cdlemg9a  41005  cdlemg9b  41006  cdlemg10a  41013  cdlemg10  41014  cdlemg12a  41016  cdlemg12b  41017  cdlemg12f  41021  cdlemg12g  41022  cdlemg12  41023  cdlemg17dN  41036  cdlemg17dALTN  41037  cdlemg17e  41038  cdlemg17f  41039  cdlemg17g  41040  cdlemg17h  41041  cdlemg17i  41042  cdlemg17pq  41045  cdlemg17iqN  41047  cdlemg17  41050  cdlemg18b  41052  cdlemg18c  41053  cdlemg19a  41056  cdlemg19  41057  cdlemg28a  41066  cdlemg27b  41069  cdlemg28b  41076  cdlemg28  41077  cdlemg33a  41079  cdlemg33b  41080  cdlemg33c  41081  cdlemg33d  41082  cdlemg33e  41083  cdlemg33  41084  cdlemg35  41086  cdlemg36  41087  cdlemg44a  41104  cdlemh  41190  cdlemi2  41192  cdlemj1  41194  tendocan  41197  cdlemk5a  41208  cdlemki  41214  cdlemkvcl  41215  cdlemk10  41216  cdlemksv2  41220  cdlemkole  41226  cdlemk14  41227  cdlemk15  41228  cdlemk16a  41229  cdlemk16  41230  cdlemk17  41231  cdlemk18  41241  cdlemk19  41242  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk30  41267  cdlemk18-3N  41273  cdlemk23-3  41275  cdlemk25-3  41277  cdlemk27-3  41280  cdlemk37  41287  cdlemkfid1N  41294  cdlemkid1  41295  cdlemky  41299  cdlemk11ta  41302  cdlemk47  41322  cdlemk48  41323  cdlemk49  41324  cdlemk50  41325  cdlemk51  41326  cdlemk52  41327  cdlemk53a  41328  cdlemk54  41331  cdlemk39u1  41340  cdlemk19u1  41342  cdleml1N  41349  cdleml2N  41350  cdleml3N  41351  dia2dimlem6  41442  cdlemn2  41568  cdlemn2a  41569  cdlemn5pre  41573  cdlemn10  41579  cdlemn11c  41582  cdlemn11pre  41583  dihjustlem  41589  dihjust  41590  lclkrlem2y  41904  aks6d1c1  42483  relexpmulnn  44062  ormkglobd  47230  natglobalincr  47232  lincreslvec3  48839  iscnrm3llem1  49305  iscnrm3l  49307  swapffunc  49638  fucofunc  49715  amgmwlem  50158