Theorem simp22 1207

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 1137	. 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp122  1306  simp222  1315  simp322  1324  elfiun  9499  cofsmo  10338  modexp  14287  funcoppc  17939  funcres  17960  catcisolem  18177  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  mulgdirlem  19145  pmtrprfv3  19496  mdetunilem4  22642  mdetuni0  22648  mdetmul  22650  prdsxmetlem  24399  isosctrlem3  26881  isosctr  26882  amgmlem  27051  f1otrg  28897  colinearalg  28943  ax5seglem6  28967  ax5seg  28971  axpasch  28974  axeuclidlem  28995  axeuclid  28996  ogrpsub  33066  ogrpaddlt  33067  ogrpsublt  33071  rhmdvd  33313  bnj966  34920  mclspps  35552  cgrtr  35956  cgrtr3  35958  ofscom  35971  cgrextend  35972  btwnxfr  36020  colinearxfr  36039  lineext  36040  fscgr  36044  linecgr  36045  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem7  36057  seglecgr12im  36074  seglecgr12  36075  segletr  36078  broutsideof3  36090  outsideofeq  36094  lineunray  36111  linecom  36114  eqlkr  39055  lshpkrlem5  39070  omlmod1i2N  39216  cvrnbtwn3  39232  cvrcmp2  39240  cvlexch2  39285  cvlexchb2  39287  cvlatexchb2  39291  cvlatexch1  39292  cvlatexch2  39293  cvlatexch3  39294  cvlsupr7  39304  cvlsupr8  39305  atnlej1  39336  atnlej2  39337  2llnneN  39366  cvratlem  39378  atcvrneN  39387  atlelt  39395  2atjm  39402  3noncolr2  39406  3noncolr1N  39407  hlatcon2  39409  3dimlem2  39416  3dim1  39424  3dim2  39425  1cvrat  39433  ps-1  39434  ps-2  39435  2atjlej  39436  hlatexch3N  39437  ps-2b  39439  3atlem1  39440  3atlem5  39444  3atlem6  39445  2atm  39484  ps-2c  39485  lplni2  39494  lplnri3N  39512  llncvrlpln2  39514  2atmat  39518  2llnm2N  39525  2llnm3N  39526  2llnm4  39527  2llnmeqat  39528  lvolnle3at  39539  4atlem0ae  39551  4atlem0be  39552  4atlem3b  39555  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem12a  39567  4at2  39571  2lplnm2N  39578  lneq2at  39735  2llnma1b  39743  2llnma1  39744  2llnma3r  39745  2llnma2  39746  2llnma2rN  39747  cdlema1N  39748  paddasslem2  39778  paddasslem16  39792  pmodlem1  39803  pmod2iN  39806  hlmod1i  39813  atmod2i1  39818  atmod2i2  39819  atmod3i1  39821  atmod3i2  39822  atmod4i1  39823  atmod4i2  39824  llnexchb2lem  39825  llnexch2N  39827  dalawlem3  39830  dalawlem4  39831  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem9  39836  dalawlem11  39838  dalawlem12  39839  dalawlem13  39840  dalawlem15  39842  osumcllem7N  39919  osumcllem9N  39921  pl42lem1N  39936  4atexlemswapqr  40020  4atex2  40034  4atex2-0bOLDN  40036  trlval4  40145  cdlemc5  40152  cdlemc6  40153  cdlemd2  40156  cdlemd4  40158  cdlemd6  40160  cdleme00a  40166  cdleme0e  40174  cdleme4  40195  cdleme4a  40196  cdleme5  40197  cdleme9  40210  cdleme16aN  40216  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11g  40222  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme11l  40226  cdleme11  40227  cdleme12  40228  cdleme13  40229  cdleme14  40230  cdleme15a  40231  cdleme15c  40233  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme17d1  40246  cdleme0nex  40247  cdleme18a  40248  cdleme18b  40249  cdleme18c  40250  cdleme18d  40252  cdlemednpq  40256  cdlemednuN  40257  cdleme20zN  40258  cdleme20y  40259  cdleme19a  40260  cdleme19b  40261  cdleme19d  40263  cdleme19e  40264  cdleme20aN  40266  cdleme20d  40269  cdleme20f  40271  cdleme20g  40272  cdleme20i  40274  cdleme20j  40275  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21b  40283  cdleme21c  40284  cdleme21e  40288  cdleme21j  40293  cdleme22aa  40296  cdleme22a  40297  cdleme22b  40298  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme27N  40326  cdleme28a  40327  cdleme28b  40328  cdleme30a  40335  cdlemefs31fv1  40381  cdleme32b  40399  cdleme32c  40400  cdleme32e  40402  cdleme35h  40413  cdleme36a  40417  cdleme36m  40418  cdleme41sn3aw  40431  cdleme41sn4aw  40432  cdleme41fva11  40434  cdleme42k  40441  cdleme43cN  40448  cdleme46f2g1  40451  cdlemeg46fjgN  40478  cdlemeg46fjv  40480  cdlemeg46frv  40482  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdleme50trn2a  40507  cdlemg4a  40565  cdlemg4d  40570  cdlemg4e  40571  cdlemg4f  40572  cdlemg8c  40586  cdlemg9a  40589  cdlemg9b  40590  cdlemg10a  40597  cdlemg10  40598  cdlemg12b  40601  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg17dN  40620  cdlemg17dALTN  40621  cdlemg17e  40622  cdlemg17f  40623  cdlemg17g  40624  cdlemg17i  40626  cdlemg17ir  40627  cdlemg17pq  40629  cdlemg17bq  40630  cdlemg17iqN  40631  cdlemg17  40634  cdlemg18b  40636  cdlemg18c  40637  cdlemg18d  40638  cdlemg18  40639  cdlemg19  40641  cdlemg21  40643  cdlemg28a  40650  cdlemg31b0a  40652  cdlemg27b  40653  cdlemg33b0  40658  cdlemg28b  40660  cdlemg28  40661  cdlemg35  40670  cdlemg36  40671  cdlemg44a  40688  cdlemh  40774  cdlemi2  40776  cdlemj1  40778  tendocan  40781  cdlemk5a  40792  cdlemk5  40793  cdlemki  40798  cdlemkvcl  40799  cdlemk10  40800  cdlemksv2  40804  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemkoatnle  40808  cdlemk15  40812  cdlemk16a  40813  cdlemk16  40814  cdlemk1u  40816  cdlemk5u  40818  cdlemk6u  40819  cdlemk18  40825  cdlemk19  40826  cdlemk7u  40827  cdlemk11u  40828  cdlemk12u  40829  cdlemk21N  40830  cdlemk20  40831  cdlemkoatnle-2N  40832  cdlemk13-2N  40833  cdlemkole-2N  40834  cdlemk14-2N  40835  cdlemk15-2N  40836  cdlemk16-2N  40837  cdlemk17-2N  40838  cdlemk18-2N  40843  cdlemk19-2N  40844  cdlemk22  40850  cdlemk30  40851  cdlemkuel-3  40855  cdlemkuv2-3N  40856  cdlemk18-3N  40857  cdlemkfid1N  40878  cdlemkid1  40879  cdlemkfid3N  40882  cdlemky  40883  cdlemk11ta  40886  cdlemk47  40906  cdlemk48  40907  cdlemk49  40908  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk53a  40912  cdlemk53  40914  cdlemk54  40915  cdlemk55a  40916  cdlemkyyN  40919  cdlemk43N  40920  cdlemk55u1  40922  cdlemk55u  40923  cdlemk39u1  40924  cdlemk19u1  40926  cdleml1N  40933  cdleml2N  40934  cdleml3N  40935  dia2dimlem6  41026  cdlemn2  41152  cdlemn2a  41153  cdlemn5pre  41157  cdlemn11a  41164  dihjustlem  41173  dihjust  41174  dihmeetlem15N  41278  lclkrlem2y  41488  aks6d1c1  42073  relexpmulnn  43671  natglobalincr  46796  iscnrm3llem1  48629  iscnrm3l  48631  amgmwlem  48896