Theorem simp21 1202

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp121  1301  simp221  1310  simp321  1319  omeulem1  8202  cofsmo  9685  axdc4lem  9871  0catg  16952  funcoppc  17139  funcres  17160  catcisolem  17360  1stfcl  17441  2ndfcl  17442  prfcl  17447  evlfcl  17466  curf1cl  17472  curfcl  17476  hofcl  17503  mulgdirlem  18252  mdetunilem4  21218  mdetuni0  21224  mdetmul  21226  prdsxmetlem  22972  isosctrlem3  25392  isosctr  25393  amgmlem  25561  f1otrg  26651  colinearalg  26690  ax5seglem6  26714  ax5seg  26718  axpasch  26721  axeuclidlem  26742  axeuclid  26743  uhgr2edg  26984  numclwlk1lem2  28143  ogrpsub  30712  ogrpaddlt  30713  ogrpsublt  30717  rhmdvd  30889  bnj1128  32257  mclspps  32826  nosupbnd2lem1  33210  cgrtr  33448  cgrtr3  33450  ofscom  33463  segconeq  33466  ifscgr  33500  btwnxfr  33512  colinearxfr  33531  lineext  33532  brofs2  33533  brifs2  33534  fscgr  33536  linecgr  33537  btwnconn1lem1  33543  btwnconn1lem2  33544  btwnconn1lem3  33545  btwnconn1lem4  33546  btwnconn1lem5  33547  btwnconn1lem6  33548  btwnconn1lem7  33549  seglecgr12im  33566  seglecgr12  33567  segletr  33570  broutsideof3  33582  outsideofeq  33586  lineunray  33603  lineelsb2  33604  linecom  33606  lshpkrlem5  36244  omlmod1i2N  36390  cvrnbtwn3  36406  cvrcmp  36413  cvrcmp2  36414  cvlexch2  36459  cvlexchb2  36461  cvlatexchb2  36465  cvlatexch2  36467  cvlatexch3  36468  cvlsupr7  36478  atnlej1  36509  atnlej2  36510  2llnneN  36539  cvratlem  36551  atcvrneN  36560  atcvrj1  36561  atlelt  36568  2atjm  36575  3noncolr2  36579  3noncolr1N  36580  3dimlem2  36589  3dim1  36597  3dim2  36598  1cvrat  36606  ps-1  36607  ps-2  36608  2atjlej  36609  hlatexch3N  36610  ps-2b  36612  3atlem1  36613  3atlem2  36614  3atlem5  36617  3atlem6  36618  llnle  36648  2atm  36657  ps-2c  36658  lplni2  36667  lplnle  36670  lplnnle2at  36671  lplnri3N  36685  llncvrlpln2  36687  2atmat  36691  2llnm2N  36698  2llnm4  36700  2llnmeqat  36701  lvolnle3at  36712  4atlem0ae  36724  4atlem0be  36725  4atlem3b  36728  4atlem9  36733  4atlem10a  36734  4atlem10  36736  4atlem11a  36737  4atlem12a  36740  4at2  36744  2lplnm2N  36751  lneq2at  36908  2llnma1b  36916  2llnma1  36917  2llnma3r  36918  2llnma2  36919  2llnma2rN  36920  cdlema1N  36921  paddasslem2  36951  paddasslem15  36964  paddasslem16  36965  pmodlem1  36976  pmodlem2  36977  pmod2iN  36979  hlmod1i  36986  atmod1i1m  36988  atmod2i1  36991  atmod2i2  36992  atmod3i1  36994  atmod3i2  36995  atmod4i1  36996  atmod4i2  36997  llnexchb2lem  36998  llnexch2N  37000  dalawlem3  37003  dalawlem4  37004  dalawlem5  37005  dalawlem6  37006  dalawlem7  37007  dalawlem8  37008  dalawlem9  37009  dalawlem11  37011  dalawlem12  37012  dalawlem13  37013  dalawlem15  37015  osumcllem9N  37094  pl42lem1N  37109  4atexlems  37182  4atex2  37207  4atex2-0bOLDN  37209  trlval4  37318  cdlemc5  37325  cdlemc6  37326  cdlemd2  37329  cdlemd4  37331  cdlemd6  37333  cdleme00a  37339  cdleme0e  37347  cdleme3g  37364  cdleme3h  37365  cdleme3  37367  cdleme4  37368  cdleme4a  37369  cdleme5  37370  cdleme9  37383  cdleme16aN  37389  cdleme11c  37391  cdleme11e  37393  cdleme11g  37395  cdleme11h  37396  cdleme11j  37397  cdleme11k  37398  cdleme11l  37399  cdleme11  37400  cdleme12  37401  cdleme14  37403  cdleme15c  37406  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme0nex  37420  cdleme18a  37421  cdleme18c  37423  cdleme18d  37425  cdlemednpq  37429  cdlemednuN  37430  cdleme20zN  37431  cdleme20y  37432  cdleme19a  37433  cdleme19b  37434  cdleme19d  37436  cdleme19e  37437  cdleme20aN  37439  cdleme20bN  37440  cdleme20c  37441  cdleme20d  37442  cdleme20f  37444  cdleme20g  37445  cdleme20i  37447  cdleme20j  37448  cdleme20l1  37450  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21b  37456  cdleme21c  37457  cdleme21e  37461  cdleme21f  37462  cdleme22a  37470  cdleme22b  37471  cdleme22e  37474  cdleme22eALTN  37475  cdleme22f  37476  cdleme26eALTN  37491  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme27N  37499  cdleme28a  37500  cdleme28b  37501  cdleme30a  37508  cdleme43fsv1snlem  37550  cdlemefs31fv1  37554  cdlemefs45eN  37561  cdleme32b  37572  cdleme32c  37573  cdleme32d  37574  cdleme35h  37586  cdleme36a  37590  cdleme36m  37591  cdleme37m  37592  cdleme40m  37597  cdleme40n  37598  cdleme41sn3aw  37604  cdleme41sn4aw  37605  cdleme41fva11  37607  cdleme42k  37614  cdleme43cN  37621  cdleme43dN  37622  cdleme46f2g1  37624  cdlemeg47rv2  37640  cdlemeg46sfg  37650  cdlemeg46fjgN  37651  cdlemeg46rjgN  37652  cdlemeg46fjv  37653  cdlemeg46frv  37655  cdlemeg46vrg  37657  cdlemeg46rgv  37658  cdlemeg46req  37659  cdlemeg46gfv  37660  cdlemg4a  37738  cdlemg4d  37743  cdlemg4e  37744  cdlemg4f  37745  cdlemg4g  37746  cdlemg4  37747  cdlemg6d  37751  cdlemg6e  37752  cdlemg8b  37758  cdlemg8c  37759  cdlemg9a  37762  cdlemg9b  37763  cdlemg10a  37770  cdlemg10  37771  cdlemg12a  37773  cdlemg12b  37774  cdlemg12f  37778  cdlemg12g  37779  cdlemg12  37780  cdlemg17dN  37793  cdlemg17dALTN  37794  cdlemg17e  37795  cdlemg17f  37796  cdlemg17g  37797  cdlemg17h  37798  cdlemg17i  37799  cdlemg17pq  37802  cdlemg17iqN  37804  cdlemg17  37807  cdlemg18b  37809  cdlemg18c  37810  cdlemg19a  37813  cdlemg19  37814  cdlemg28a  37823  cdlemg27b  37826  cdlemg28b  37833  cdlemg28  37834  cdlemg33a  37836  cdlemg33b  37837  cdlemg33c  37838  cdlemg33d  37839  cdlemg33e  37840  cdlemg33  37841  cdlemg35  37843  cdlemg36  37844  cdlemg44a  37861  cdlemh  37947  cdlemi2  37949  cdlemj1  37951  tendocan  37954  cdlemk5a  37965  cdlemki  37971  cdlemkvcl  37972  cdlemk10  37973  cdlemksv2  37977  cdlemkole  37983  cdlemk14  37984  cdlemk15  37985  cdlemk16a  37986  cdlemk16  37987  cdlemk17  37988  cdlemk18  37998  cdlemk19  37999  cdlemkoatnle-2N  38005  cdlemk13-2N  38006  cdlemkole-2N  38007  cdlemk14-2N  38008  cdlemk15-2N  38009  cdlemk16-2N  38010  cdlemk17-2N  38011  cdlemk18-2N  38016  cdlemk19-2N  38017  cdlemk30  38024  cdlemk18-3N  38030  cdlemk23-3  38032  cdlemk25-3  38034  cdlemk27-3  38037  cdlemk37  38044  cdlemkfid1N  38051  cdlemkid1  38052  cdlemky  38056  cdlemk11ta  38059  cdlemk47  38079  cdlemk48  38080  cdlemk49  38081  cdlemk50  38082  cdlemk51  38083  cdlemk52  38084  cdlemk53a  38085  cdlemk54  38088  cdlemk39u1  38097  cdlemk19u1  38099  cdleml1N  38106  cdleml2N  38107  cdleml3N  38108  dia2dimlem6  38199  cdlemn2  38325  cdlemn2a  38326  cdlemn5pre  38330  cdlemn10  38336  cdlemn11c  38339  cdlemn11pre  38340  dihjustlem  38346  dihjust  38347  lclkrlem2y  38661  relexpmulnn  40047  lincreslvec3  44531  amgmwlem  44897