Theorem simp21 1186

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simp121  1285  simp221  1294  simp321  1303  omeulem1  8011  cofsmo  9491  axdc4lem  9677  0catg  16819  funcoppc  17006  funcres  17027  catcisolem  17227  1stfcl  17308  2ndfcl  17309  prfcl  17314  evlfcl  17333  curf1cl  17339  curfcl  17343  hofcl  17370  mulgdirlem  18045  mdetunilem4  20931  mdetuni0  20937  mdetmul  20939  prdsxmetlem  22684  isosctrlem3  25102  isosctr  25103  amgmlem  25272  f1otrg  26363  colinearalg  26402  ax5seglem6  26426  ax5seg  26430  axpasch  26433  axeuclidlem  26454  axeuclid  26455  uhgr2edg  26696  numclwlk1lem2  27926  ogrpsub  30436  ogrpaddlt  30437  ogrpsublt  30441  rhmdvd  30573  bnj1128  31907  mclspps  32351  nosupbnd2lem1  32736  cgrtr  32974  cgrtr3  32976  ofscom  32989  segconeq  32992  ifscgr  33026  btwnxfr  33038  colinearxfr  33057  lineext  33058  brofs2  33059  brifs2  33060  fscgr  33062  linecgr  33063  btwnconn1lem1  33069  btwnconn1lem2  33070  btwnconn1lem3  33071  btwnconn1lem4  33072  btwnconn1lem5  33073  btwnconn1lem6  33074  btwnconn1lem7  33075  seglecgr12im  33092  seglecgr12  33093  segletr  33096  broutsideof3  33108  outsideofeq  33112  lineunray  33129  lineelsb2  33130  linecom  33132  lshpkrlem5  35695  omlmod1i2N  35841  cvrnbtwn3  35857  cvrcmp  35864  cvrcmp2  35865  cvlexch2  35910  cvlexchb2  35912  cvlatexchb2  35916  cvlatexch2  35918  cvlatexch3  35919  cvlsupr7  35929  atnlej1  35960  atnlej2  35961  2llnneN  35990  cvratlem  36002  atcvrneN  36011  atcvrj1  36012  atlelt  36019  2atjm  36026  3noncolr2  36030  3noncolr1N  36031  3dimlem2  36040  3dim1  36048  3dim2  36049  1cvrat  36057  ps-1  36058  ps-2  36059  2atjlej  36060  hlatexch3N  36061  ps-2b  36063  3atlem1  36064  3atlem2  36065  3atlem5  36068  3atlem6  36069  llnle  36099  2atm  36108  ps-2c  36109  lplni2  36118  lplnle  36121  lplnnle2at  36122  lplnri3N  36136  llncvrlpln2  36138  2atmat  36142  2llnm2N  36149  2llnm4  36151  2llnmeqat  36152  lvolnle3at  36163  4atlem0ae  36175  4atlem0be  36176  4atlem3b  36179  4atlem9  36184  4atlem10a  36185  4atlem10  36187  4atlem11a  36188  4atlem12a  36191  4at2  36195  2lplnm2N  36202  lneq2at  36359  2llnma1b  36367  2llnma1  36368  2llnma3r  36369  2llnma2  36370  2llnma2rN  36371  cdlema1N  36372  paddasslem2  36402  paddasslem15  36415  paddasslem16  36416  pmodlem1  36427  pmodlem2  36428  pmod2iN  36430  hlmod1i  36437  atmod1i1m  36439  atmod2i1  36442  atmod2i2  36443  atmod3i1  36445  atmod3i2  36446  atmod4i1  36447  atmod4i2  36448  llnexchb2lem  36449  llnexch2N  36451  dalawlem3  36454  dalawlem4  36455  dalawlem5  36456  dalawlem6  36457  dalawlem7  36458  dalawlem8  36459  dalawlem9  36460  dalawlem11  36462  dalawlem12  36463  dalawlem13  36464  dalawlem15  36466  osumcllem9N  36545  pl42lem1N  36560  4atexlems  36633  4atex2  36658  4atex2-0bOLDN  36660  trlval4  36769  cdlemc5  36776  cdlemc6  36777  cdlemd2  36780  cdlemd4  36782  cdlemd6  36784  cdleme00a  36790  cdleme0e  36798  cdleme3g  36815  cdleme3h  36816  cdleme3  36818  cdleme4  36819  cdleme4a  36820  cdleme5  36821  cdleme9  36834  cdleme16aN  36840  cdleme11c  36842  cdleme11e  36844  cdleme11g  36846  cdleme11h  36847  cdleme11j  36848  cdleme11k  36849  cdleme11l  36850  cdleme11  36851  cdleme12  36852  cdleme14  36854  cdleme15c  36857  cdleme16b  36860  cdleme16c  36861  cdleme16d  36862  cdleme16e  36863  cdleme16f  36864  cdleme0nex  36871  cdleme18a  36872  cdleme18c  36874  cdleme18d  36876  cdlemednpq  36880  cdlemednuN  36881  cdleme20zN  36882  cdleme20y  36883  cdleme19a  36884  cdleme19b  36885  cdleme19d  36887  cdleme19e  36888  cdleme20aN  36890  cdleme20bN  36891  cdleme20c  36892  cdleme20d  36893  cdleme20f  36895  cdleme20g  36896  cdleme20i  36898  cdleme20j  36899  cdleme20l1  36901  cdleme20l2  36902  cdleme20l  36903  cdleme20m  36904  cdleme21b  36907  cdleme21c  36908  cdleme21e  36912  cdleme21f  36913  cdleme22a  36921  cdleme22b  36922  cdleme22e  36925  cdleme22eALTN  36926  cdleme22f  36927  cdleme26eALTN  36942  cdleme26fALTN  36943  cdleme26f  36944  cdleme26f2ALTN  36945  cdleme26f2  36946  cdleme27N  36950  cdleme28a  36951  cdleme28b  36952  cdleme30a  36959  cdleme43fsv1snlem  37001  cdlemefs31fv1  37005  cdlemefs45eN  37012  cdleme32b  37023  cdleme32c  37024  cdleme32d  37025  cdleme35h  37037  cdleme36a  37041  cdleme36m  37042  cdleme37m  37043  cdleme40m  37048  cdleme40n  37049  cdleme41sn3aw  37055  cdleme41sn4aw  37056  cdleme41fva11  37058  cdleme42k  37065  cdleme43cN  37072  cdleme43dN  37073  cdleme46f2g1  37075  cdlemeg47rv2  37091  cdlemeg46sfg  37101  cdlemeg46fjgN  37102  cdlemeg46rjgN  37103  cdlemeg46fjv  37104  cdlemeg46frv  37106  cdlemeg46vrg  37108  cdlemeg46rgv  37109  cdlemeg46req  37110  cdlemeg46gfv  37111  cdlemg4a  37189  cdlemg4d  37194  cdlemg4e  37195  cdlemg4f  37196  cdlemg4g  37197  cdlemg4  37198  cdlemg6d  37202  cdlemg6e  37203  cdlemg8b  37209  cdlemg8c  37210  cdlemg9a  37213  cdlemg9b  37214  cdlemg10a  37221  cdlemg10  37222  cdlemg12a  37224  cdlemg12b  37225  cdlemg12f  37229  cdlemg12g  37230  cdlemg12  37231  cdlemg17dN  37244  cdlemg17dALTN  37245  cdlemg17e  37246  cdlemg17f  37247  cdlemg17g  37248  cdlemg17h  37249  cdlemg17i  37250  cdlemg17pq  37253  cdlemg17iqN  37255  cdlemg17  37258  cdlemg18b  37260  cdlemg18c  37261  cdlemg19a  37264  cdlemg19  37265  cdlemg28a  37274  cdlemg27b  37277  cdlemg28b  37284  cdlemg28  37285  cdlemg33a  37287  cdlemg33b  37288  cdlemg33c  37289  cdlemg33d  37290  cdlemg33e  37291  cdlemg33  37292  cdlemg35  37294  cdlemg36  37295  cdlemg44a  37312  cdlemh  37398  cdlemi2  37400  cdlemj1  37402  tendocan  37405  cdlemk5a  37416  cdlemki  37422  cdlemkvcl  37423  cdlemk10  37424  cdlemksv2  37428  cdlemkole  37434  cdlemk14  37435  cdlemk15  37436  cdlemk16a  37437  cdlemk16  37438  cdlemk17  37439  cdlemk18  37449  cdlemk19  37450  cdlemkoatnle-2N  37456  cdlemk13-2N  37457  cdlemkole-2N  37458  cdlemk14-2N  37459  cdlemk15-2N  37460  cdlemk16-2N  37461  cdlemk17-2N  37462  cdlemk18-2N  37467  cdlemk19-2N  37468  cdlemk30  37475  cdlemk18-3N  37481  cdlemk23-3  37483  cdlemk25-3  37485  cdlemk27-3  37488  cdlemk37  37495  cdlemkfid1N  37502  cdlemkid1  37503  cdlemky  37507  cdlemk11ta  37510  cdlemk47  37530  cdlemk48  37531  cdlemk49  37532  cdlemk50  37533  cdlemk51  37534  cdlemk52  37535  cdlemk53a  37536  cdlemk54  37539  cdlemk39u1  37548  cdlemk19u1  37550  cdleml1N  37557  cdleml2N  37558  cdleml3N  37559  dia2dimlem6  37650  cdlemn2  37776  cdlemn2a  37777  cdlemn5pre  37781  cdlemn10  37787  cdlemn11c  37790  cdlemn11pre  37791  dihjustlem  37797  dihjust  37798  lclkrlem2y  38112  relexpmulnn  39417  lincreslvec3  43905  amgmwlem  44271