Theorem simp22 1208

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp22	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simp22

Step	Hyp	Ref	Expression
1		simp2 1138	. 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:  simp122  1307  simp222  1316  simp322  1325  elfiun  9425  cofsmo  10264  modexp  14201  funcoppc  17825  funcres  17846  catcisolem  18060  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  mulgdirlem  18985  pmtrprfv3  19322  mdetunilem4  22117  mdetuni0  22123  mdetmul  22125  prdsxmetlem  23874  isosctrlem3  26325  isosctr  26326  amgmlem  26494  f1otrg  28153  colinearalg  28199  ax5seglem6  28223  ax5seg  28227  axpasch  28230  axeuclidlem  28251  axeuclid  28252  ogrpsub  32265  ogrpaddlt  32266  ogrpsublt  32270  rhmdvd  32467  bnj966  33986  mclspps  34606  cgrtr  34995  cgrtr3  34997  ofscom  35010  cgrextend  35011  btwnxfr  35059  colinearxfr  35078  lineext  35079  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  linecom  35153  eqlkr  38017  lshpkrlem5  38032  omlmod1i2N  38178  cvrnbtwn3  38194  cvrcmp2  38202  cvlexch2  38247  cvlexchb2  38249  cvlatexchb2  38253  cvlatexch1  38254  cvlatexch2  38255  cvlatexch3  38256  cvlsupr7  38266  cvlsupr8  38267  atnlej1  38298  atnlej2  38299  2llnneN  38328  cvratlem  38340  atcvrneN  38349  atlelt  38357  2atjm  38364  3noncolr2  38368  3noncolr1N  38369  hlatcon2  38371  3dimlem2  38378  3dim1  38386  3dim2  38387  1cvrat  38395  ps-1  38396  ps-2  38397  2atjlej  38398  hlatexch3N  38399  ps-2b  38401  3atlem1  38402  3atlem5  38406  3atlem6  38407  2atm  38446  ps-2c  38447  lplni2  38456  lplnri3N  38474  llncvrlpln2  38476  2atmat  38480  2llnm2N  38487  2llnm3N  38488  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  paddasslem16  38754  pmodlem1  38765  pmod2iN  38768  hlmod1i  38775  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  osumcllem7N  38881  osumcllem9N  38883  pl42lem1N  38898  4atexlemswapqr  38982  4atex2  38996  4atex2-0bOLDN  38998  trlval4  39107  cdlemc5  39114  cdlemc6  39115  cdlemd2  39118  cdlemd4  39120  cdlemd6  39122  cdleme00a  39128  cdleme0e  39136  cdleme4  39157  cdleme4a  39158  cdleme5  39159  cdleme9  39172  cdleme16aN  39178  cdleme11c  39180  cdleme11dN  39181  cdleme11e  39182  cdleme11g  39184  cdleme11h  39185  cdleme11j  39186  cdleme11k  39187  cdleme11l  39188  cdleme11  39189  cdleme12  39190  cdleme13  39191  cdleme14  39192  cdleme15a  39193  cdleme15c  39195  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme17d1  39208  cdleme0nex  39209  cdleme18a  39210  cdleme18b  39211  cdleme18c  39212  cdleme18d  39214  cdlemednpq  39218  cdlemednuN  39219  cdleme20zN  39220  cdleme20y  39221  cdleme19a  39222  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20aN  39228  cdleme20d  39231  cdleme20f  39233  cdleme20g  39234  cdleme20i  39236  cdleme20j  39237  cdleme20l1  39239  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme21b  39245  cdleme21c  39246  cdleme21e  39250  cdleme21j  39255  cdleme22aa  39258  cdleme22a  39259  cdleme22b  39260  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme27N  39288  cdleme28a  39289  cdleme28b  39290  cdleme30a  39297  cdlemefs31fv1  39343  cdleme32b  39361  cdleme32c  39362  cdleme32e  39364  cdleme35h  39375  cdleme36a  39379  cdleme36m  39380  cdleme41sn3aw  39393  cdleme41sn4aw  39394  cdleme41fva11  39396  cdleme42k  39403  cdleme43cN  39410  cdleme46f2g1  39413  cdlemeg46fjgN  39440  cdlemeg46fjv  39442  cdlemeg46frv  39444  cdlemeg46rgv  39447  cdlemeg46req  39448  cdlemeg46gfv  39449  cdleme50trn2a  39469  cdlemg4a  39527  cdlemg4d  39532  cdlemg4e  39533  cdlemg4f  39534  cdlemg8c  39548  cdlemg9a  39551  cdlemg9b  39552  cdlemg10a  39559  cdlemg10  39560  cdlemg12b  39563  cdlemg12f  39567  cdlemg12g  39568  cdlemg12  39569  cdlemg17dN  39582  cdlemg17dALTN  39583  cdlemg17e  39584  cdlemg17f  39585  cdlemg17g  39586  cdlemg17i  39588  cdlemg17ir  39589  cdlemg17pq  39591  cdlemg17bq  39592  cdlemg17iqN  39593  cdlemg17  39596  cdlemg18b  39598  cdlemg18c  39599  cdlemg18d  39600  cdlemg18  39601  cdlemg19  39603  cdlemg21  39605  cdlemg28a  39612  cdlemg31b0a  39614  cdlemg27b  39615  cdlemg33b0  39620  cdlemg28b  39622  cdlemg28  39623  cdlemg35  39632  cdlemg36  39633  cdlemg44a  39650  cdlemh  39736  cdlemi2  39738  cdlemj1  39740  tendocan  39743  cdlemk5a  39754  cdlemk5  39755  cdlemki  39760  cdlemkvcl  39761  cdlemk10  39762  cdlemksv2  39766  cdlemk7  39767  cdlemk11  39768  cdlemk12  39769  cdlemkoatnle  39770  cdlemk15  39774  cdlemk16a  39775  cdlemk16  39776  cdlemk1u  39778  cdlemk5u  39780  cdlemk6u  39781  cdlemk18  39787  cdlemk19  39788  cdlemk7u  39789  cdlemk11u  39790  cdlemk12u  39791  cdlemk21N  39792  cdlemk20  39793  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  cdlemk22  39812  cdlemk30  39813  cdlemkuel-3  39817  cdlemkuv2-3N  39818  cdlemk18-3N  39819  cdlemkfid1N  39840  cdlemkid1  39841  cdlemkfid3N  39844  cdlemky  39845  cdlemk11ta  39848  cdlemk47  39868  cdlemk48  39869  cdlemk49  39870  cdlemk50  39871  cdlemk51  39872  cdlemk52  39873  cdlemk53a  39874  cdlemk53  39876  cdlemk54  39877  cdlemk55a  39878  cdlemkyyN  39881  cdlemk43N  39882  cdlemk55u1  39884  cdlemk55u  39885  cdlemk39u1  39886  cdlemk19u1  39888  cdleml1N  39895  cdleml2N  39896  cdleml3N  39897  dia2dimlem6  39988  cdlemn2  40114  cdlemn2a  40115  cdlemn5pre  40119  cdlemn11a  40126  dihjustlem  40135  dihjust  40136  dihmeetlem15N  40240  lclkrlem2y  40450  relexpmulnn  42508  natglobalincr  45639  iscnrm3llem1  47630  iscnrm3l  47632  amgmwlem  47897