Theorem simp21 1206

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 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp121  1305  simp221  1314  simp321  1323  omeulem1  8534  cofsmo  10214  axdc4lem  10400  0catg  17582  funcoppc  17775  funcres  17796  catcisolem  18010  1stfcl  18099  2ndfcl  18100  prfcl  18105  evlfcl  18125  curf1cl  18131  curfcl  18135  hofcl  18162  mulgdirlem  18921  mdetunilem4  22001  mdetuni0  22007  mdetmul  22009  prdsxmetlem  23758  isosctrlem3  26207  isosctr  26208  amgmlem  26376  nosupbnd2lem1  27100  addsass  27356  f1otrg  27876  colinearalg  27922  ax5seglem6  27946  ax5seg  27950  axpasch  27953  axeuclidlem  27974  axeuclid  27975  uhgr2edg  28219  numclwlk1lem2  29377  ogrpsub  31994  ogrpaddlt  31995  ogrpsublt  31999  rhmdvd  32184  bnj1128  33691  mclspps  34265  cgrtr  34653  cgrtr3  34655  ofscom  34668  segconeq  34671  ifscgr  34705  btwnxfr  34717  colinearxfr  34736  lineext  34737  brofs2  34738  brifs2  34739  fscgr  34741  linecgr  34742  btwnconn1lem1  34748  btwnconn1lem2  34749  btwnconn1lem3  34750  btwnconn1lem4  34751  btwnconn1lem5  34752  btwnconn1lem6  34753  btwnconn1lem7  34754  seglecgr12im  34771  seglecgr12  34772  segletr  34775  broutsideof3  34787  outsideofeq  34791  lineunray  34808  lineelsb2  34809  linecom  34811  lshpkrlem5  37649  omlmod1i2N  37795  cvrnbtwn3  37811  cvrcmp  37818  cvrcmp2  37819  cvlexch2  37864  cvlexchb2  37866  cvlatexchb2  37870  cvlatexch2  37872  cvlatexch3  37873  cvlsupr7  37883  atnlej1  37915  atnlej2  37916  2llnneN  37945  cvratlem  37957  atcvrneN  37966  atcvrj1  37967  atlelt  37974  2atjm  37981  3noncolr2  37985  3noncolr1N  37986  3dimlem2  37995  3dim1  38003  3dim2  38004  1cvrat  38012  ps-1  38013  ps-2  38014  2atjlej  38015  hlatexch3N  38016  ps-2b  38018  3atlem1  38019  3atlem2  38020  3atlem5  38023  3atlem6  38024  llnle  38054  2atm  38063  ps-2c  38064  lplni2  38073  lplnle  38076  lplnnle2at  38077  lplnri3N  38091  llncvrlpln2  38093  2atmat  38097  2llnm2N  38104  2llnm4  38106  2llnmeqat  38107  lvolnle3at  38118  4atlem0ae  38130  4atlem0be  38131  4atlem3b  38134  4atlem9  38139  4atlem10a  38140  4atlem10  38142  4atlem11a  38143  4atlem12a  38146  4at2  38150  2lplnm2N  38157  lneq2at  38314  2llnma1b  38322  2llnma1  38323  2llnma3r  38324  2llnma2  38325  2llnma2rN  38326  cdlema1N  38327  paddasslem2  38357  paddasslem15  38370  paddasslem16  38371  pmodlem1  38382  pmodlem2  38383  pmod2iN  38385  hlmod1i  38392  atmod1i1m  38394  atmod2i1  38397  atmod2i2  38398  atmod3i1  38400  atmod3i2  38401  atmod4i1  38402  atmod4i2  38403  llnexchb2lem  38404  llnexch2N  38406  dalawlem3  38409  dalawlem4  38410  dalawlem5  38411  dalawlem6  38412  dalawlem7  38413  dalawlem8  38414  dalawlem9  38415  dalawlem11  38417  dalawlem12  38418  dalawlem13  38419  dalawlem15  38421  osumcllem9N  38500  pl42lem1N  38515  4atexlems  38588  4atex2  38613  4atex2-0bOLDN  38615  trlval4  38724  cdlemc5  38731  cdlemc6  38732  cdlemd2  38735  cdlemd4  38737  cdlemd6  38739  cdleme00a  38745  cdleme0e  38753  cdleme3g  38770  cdleme3h  38771  cdleme3  38773  cdleme4  38774  cdleme4a  38775  cdleme5  38776  cdleme9  38789  cdleme16aN  38795  cdleme11c  38797  cdleme11e  38799  cdleme11g  38801  cdleme11h  38802  cdleme11j  38803  cdleme11k  38804  cdleme11l  38805  cdleme11  38806  cdleme12  38807  cdleme14  38809  cdleme15c  38812  cdleme16b  38815  cdleme16c  38816  cdleme16d  38817  cdleme16e  38818  cdleme16f  38819  cdleme0nex  38826  cdleme18a  38827  cdleme18c  38829  cdleme18d  38831  cdlemednpq  38835  cdlemednuN  38836  cdleme20zN  38837  cdleme20y  38838  cdleme19a  38839  cdleme19b  38840  cdleme19d  38842  cdleme19e  38843  cdleme20aN  38845  cdleme20bN  38846  cdleme20c  38847  cdleme20d  38848  cdleme20f  38850  cdleme20g  38851  cdleme20i  38853  cdleme20j  38854  cdleme20l1  38856  cdleme20l2  38857  cdleme20l  38858  cdleme20m  38859  cdleme21b  38862  cdleme21c  38863  cdleme21e  38867  cdleme21f  38868  cdleme22a  38876  cdleme22b  38877  cdleme22e  38880  cdleme22eALTN  38881  cdleme22f  38882  cdleme26eALTN  38897  cdleme26fALTN  38898  cdleme26f  38899  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme27N  38905  cdleme28a  38906  cdleme28b  38907  cdleme30a  38914  cdleme43fsv1snlem  38956  cdlemefs31fv1  38960  cdlemefs45eN  38967  cdleme32b  38978  cdleme32c  38979  cdleme32d  38980  cdleme35h  38992  cdleme36a  38996  cdleme36m  38997  cdleme37m  38998  cdleme40m  39003  cdleme40n  39004  cdleme41sn3aw  39010  cdleme41sn4aw  39011  cdleme41fva11  39013  cdleme42k  39020  cdleme43cN  39027  cdleme43dN  39028  cdleme46f2g1  39030  cdlemeg47rv2  39046  cdlemeg46sfg  39056  cdlemeg46fjgN  39057  cdlemeg46rjgN  39058  cdlemeg46fjv  39059  cdlemeg46frv  39061  cdlemeg46vrg  39063  cdlemeg46rgv  39064  cdlemeg46req  39065  cdlemeg46gfv  39066  cdlemg4a  39144  cdlemg4d  39149  cdlemg4e  39150  cdlemg4f  39151  cdlemg4g  39152  cdlemg4  39153  cdlemg6d  39157  cdlemg6e  39158  cdlemg8b  39164  cdlemg8c  39165  cdlemg9a  39168  cdlemg9b  39169  cdlemg10a  39176  cdlemg10  39177  cdlemg12a  39179  cdlemg12b  39180  cdlemg12f  39184  cdlemg12g  39185  cdlemg12  39186  cdlemg17dN  39199  cdlemg17dALTN  39200  cdlemg17e  39201  cdlemg17f  39202  cdlemg17g  39203  cdlemg17h  39204  cdlemg17i  39205  cdlemg17pq  39208  cdlemg17iqN  39210  cdlemg17  39213  cdlemg18b  39215  cdlemg18c  39216  cdlemg19a  39219  cdlemg19  39220  cdlemg28a  39229  cdlemg27b  39232  cdlemg28b  39239  cdlemg28  39240  cdlemg33a  39242  cdlemg33b  39243  cdlemg33c  39244  cdlemg33d  39245  cdlemg33e  39246  cdlemg33  39247  cdlemg35  39249  cdlemg36  39250  cdlemg44a  39267  cdlemh  39353  cdlemi2  39355  cdlemj1  39357  tendocan  39360  cdlemk5a  39371  cdlemki  39377  cdlemkvcl  39378  cdlemk10  39379  cdlemksv2  39383  cdlemkole  39389  cdlemk14  39390  cdlemk15  39391  cdlemk16a  39392  cdlemk16  39393  cdlemk17  39394  cdlemk18  39404  cdlemk19  39405  cdlemkoatnle-2N  39411  cdlemk13-2N  39412  cdlemkole-2N  39413  cdlemk14-2N  39414  cdlemk15-2N  39415  cdlemk16-2N  39416  cdlemk17-2N  39417  cdlemk18-2N  39422  cdlemk19-2N  39423  cdlemk30  39430  cdlemk18-3N  39436  cdlemk23-3  39438  cdlemk25-3  39440  cdlemk27-3  39443  cdlemk37  39450  cdlemkfid1N  39457  cdlemkid1  39458  cdlemky  39462  cdlemk11ta  39465  cdlemk47  39485  cdlemk48  39486  cdlemk49  39487  cdlemk50  39488  cdlemk51  39489  cdlemk52  39490  cdlemk53a  39491  cdlemk54  39494  cdlemk39u1  39503  cdlemk19u1  39505  cdleml1N  39512  cdleml2N  39513  cdleml3N  39514  dia2dimlem6  39605  cdlemn2  39731  cdlemn2a  39732  cdlemn5pre  39736  cdlemn10  39742  cdlemn11c  39745  cdlemn11pre  39746  dihjustlem  39752  dihjust  39753  lclkrlem2y  40067  relexpmulnn  42103  natglobalincr  45236  lincreslvec3  46683  iscnrm3llem1  47102  iscnrm3l  47104  amgmwlem  47369