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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8582  cofsmo  10264  axdc4lem  10450  0catg  17632  funcoppc  17825  funcres  17846  catcisolem  18060  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  mulgdirlem  18985  mdetunilem4  22117  mdetuni0  22123  mdetmul  22125  prdsxmetlem  23874  isosctrlem3  26325  isosctr  26326  amgmlem  26494  nosupbnd2lem1  27218  addsass  27491  f1otrg  28153  colinearalg  28199  ax5seglem6  28223  ax5seg  28227  axpasch  28230  axeuclidlem  28251  axeuclid  28252  uhgr2edg  28496  numclwlk1lem2  29654  ogrpsub  32265  ogrpaddlt  32266  ogrpsublt  32270  rhmdvd  32467  bnj1128  34032  mclspps  34606  cgrtr  34995  cgrtr3  34997  ofscom  35010  segconeq  35013  ifscgr  35047  btwnxfr  35059  colinearxfr  35078  lineext  35079  brofs2  35080  brifs2  35081  fscgr  35083  linecgr  35084  btwnconn1lem1  35090  btwnconn1lem2  35091  btwnconn1lem3  35092  btwnconn1lem4  35093  btwnconn1lem5  35094  btwnconn1lem6  35095  btwnconn1lem7  35096  seglecgr12im  35113  seglecgr12  35114  segletr  35117  broutsideof3  35129  outsideofeq  35133  lineunray  35150  lineelsb2  35151  linecom  35153  lshpkrlem5  38032  omlmod1i2N  38178  cvrnbtwn3  38194  cvrcmp  38201  cvrcmp2  38202  cvlexch2  38247  cvlexchb2  38249  cvlatexchb2  38253  cvlatexch2  38255  cvlatexch3  38256  cvlsupr7  38266  atnlej1  38298  atnlej2  38299  2llnneN  38328  cvratlem  38340  atcvrneN  38349  atcvrj1  38350  atlelt  38357  2atjm  38364  3noncolr2  38368  3noncolr1N  38369  3dimlem2  38378  3dim1  38386  3dim2  38387  1cvrat  38395  ps-1  38396  ps-2  38397  2atjlej  38398  hlatexch3N  38399  ps-2b  38401  3atlem1  38402  3atlem2  38403  3atlem5  38406  3atlem6  38407  llnle  38437  2atm  38446  ps-2c  38447  lplni2  38456  lplnle  38459  lplnnle2at  38460  lplnri3N  38474  llncvrlpln2  38476  2atmat  38480  2llnm2N  38487  2llnm4  38489  2llnmeqat  38490  lvolnle3at  38501  4atlem0ae  38513  4atlem0be  38514  4atlem3b  38517  4atlem9  38522  4atlem10a  38523  4atlem10  38525  4atlem11a  38526  4atlem12a  38529  4at2  38533  2lplnm2N  38540  lneq2at  38697  2llnma1b  38705  2llnma1  38706  2llnma3r  38707  2llnma2  38708  2llnma2rN  38709  cdlema1N  38710  paddasslem2  38740  paddasslem15  38753  paddasslem16  38754  pmodlem1  38765  pmodlem2  38766  pmod2iN  38768  hlmod1i  38775  atmod1i1m  38777  atmod2i1  38780  atmod2i2  38781  atmod3i1  38783  atmod3i2  38784  atmod4i1  38785  atmod4i2  38786  llnexchb2lem  38787  llnexch2N  38789  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  dalawlem13  38802  dalawlem15  38804  osumcllem9N  38883  pl42lem1N  38898  4atexlems  38971  4atex2  38996  4atex2-0bOLDN  38998  trlval4  39107  cdlemc5  39114  cdlemc6  39115  cdlemd2  39118  cdlemd4  39120  cdlemd6  39122  cdleme00a  39128  cdleme0e  39136  cdleme3g  39153  cdleme3h  39154  cdleme3  39156  cdleme4  39157  cdleme4a  39158  cdleme5  39159  cdleme9  39172  cdleme16aN  39178  cdleme11c  39180  cdleme11e  39182  cdleme11g  39184  cdleme11h  39185  cdleme11j  39186  cdleme11k  39187  cdleme11l  39188  cdleme11  39189  cdleme12  39190  cdleme14  39192  cdleme15c  39195  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme0nex  39209  cdleme18a  39210  cdleme18c  39212  cdleme18d  39214  cdlemednpq  39218  cdlemednuN  39219  cdleme20zN  39220  cdleme20y  39221  cdleme19a  39222  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20aN  39228  cdleme20bN  39229  cdleme20c  39230  cdleme20d  39231  cdleme20f  39233  cdleme20g  39234  cdleme20i  39236  cdleme20j  39237  cdleme20l1  39239  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme21b  39245  cdleme21c  39246  cdleme21e  39250  cdleme21f  39251  cdleme22a  39259  cdleme22b  39260  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme26eALTN  39280  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme27N  39288  cdleme28a  39289  cdleme28b  39290  cdleme30a  39297  cdleme43fsv1snlem  39339  cdlemefs31fv1  39343  cdlemefs45eN  39350  cdleme32b  39361  cdleme32c  39362  cdleme32d  39363  cdleme35h  39375  cdleme36a  39379  cdleme36m  39380  cdleme37m  39381  cdleme40m  39386  cdleme40n  39387  cdleme41sn3aw  39393  cdleme41sn4aw  39394  cdleme41fva11  39396  cdleme42k  39403  cdleme43cN  39410  cdleme43dN  39411  cdleme46f2g1  39413  cdlemeg47rv2  39429  cdlemeg46sfg  39439  cdlemeg46fjgN  39440  cdlemeg46rjgN  39441  cdlemeg46fjv  39442  cdlemeg46frv  39444  cdlemeg46vrg  39446  cdlemeg46rgv  39447  cdlemeg46req  39448  cdlemeg46gfv  39449  cdlemg4a  39527  cdlemg4d  39532  cdlemg4e  39533  cdlemg4f  39534  cdlemg4g  39535  cdlemg4  39536  cdlemg6d  39540  cdlemg6e  39541  cdlemg8b  39547  cdlemg8c  39548  cdlemg9a  39551  cdlemg9b  39552  cdlemg10a  39559  cdlemg10  39560  cdlemg12a  39562  cdlemg12b  39563  cdlemg12f  39567  cdlemg12g  39568  cdlemg12  39569  cdlemg17dN  39582  cdlemg17dALTN  39583  cdlemg17e  39584  cdlemg17f  39585  cdlemg17g  39586  cdlemg17h  39587  cdlemg17i  39588  cdlemg17pq  39591  cdlemg17iqN  39593  cdlemg17  39596  cdlemg18b  39598  cdlemg18c  39599  cdlemg19a  39602  cdlemg19  39603  cdlemg28a  39612  cdlemg27b  39615  cdlemg28b  39622  cdlemg28  39623  cdlemg33a  39625  cdlemg33b  39626  cdlemg33c  39627  cdlemg33d  39628  cdlemg33e  39629  cdlemg33  39630  cdlemg35  39632  cdlemg36  39633  cdlemg44a  39650  cdlemh  39736  cdlemi2  39738  cdlemj1  39740  tendocan  39743  cdlemk5a  39754  cdlemki  39760  cdlemkvcl  39761  cdlemk10  39762  cdlemksv2  39766  cdlemkole  39772  cdlemk14  39773  cdlemk15  39774  cdlemk16a  39775  cdlemk16  39776  cdlemk17  39777  cdlemk18  39787  cdlemk19  39788  cdlemkoatnle-2N  39794  cdlemk13-2N  39795  cdlemkole-2N  39796  cdlemk14-2N  39797  cdlemk15-2N  39798  cdlemk16-2N  39799  cdlemk17-2N  39800  cdlemk18-2N  39805  cdlemk19-2N  39806  cdlemk30  39813  cdlemk18-3N  39819  cdlemk23-3  39821  cdlemk25-3  39823  cdlemk27-3  39826  cdlemk37  39833  cdlemkfid1N  39840  cdlemkid1  39841  cdlemky  39845  cdlemk11ta  39848  cdlemk47  39868  cdlemk48  39869  cdlemk49  39870  cdlemk50  39871  cdlemk51  39872  cdlemk52  39873  cdlemk53a  39874  cdlemk54  39877  cdlemk39u1  39886  cdlemk19u1  39888  cdleml1N  39895  cdleml2N  39896  cdleml3N  39897  dia2dimlem6  39988  cdlemn2  40114  cdlemn2a  40115  cdlemn5pre  40119  cdlemn10  40125  cdlemn11c  40128  cdlemn11pre  40129  dihjustlem  40135  dihjust  40136  lclkrlem2y  40450  relexpmulnn  42508  natglobalincr  45639  lincreslvec3  47211  iscnrm3llem1  47630  iscnrm3l  47632  amgmwlem  47897