Theorem simp22 1209

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 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  1308  simp222  1317  simp322  1326  elfiun  9345  cofsmo  10191  modexp  14173  funcoppc  17811  funcres  17832  catcisolem  18046  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  mulgdirlem  19047  pmtrprfv3  19395  ogrpsub  20078  ogrpaddlt  20079  ogrpsublt  20083  mdetunilem4  22571  mdetuni0  22577  mdetmul  22579  prdsxmetlem  24324  isosctrlem3  26798  isosctr  26799  amgmlem  26968  f1otrg  28955  colinearalg  28995  ax5seglem6  29019  ax5seg  29023  axpasch  29026  axeuclidlem  29047  axeuclid  29048  rhmdvd  33416  bnj966  35119  mclspps  35797  cgrtr  36205  cgrtr3  36207  ofscom  36220  cgrextend  36221  btwnxfr  36269  colinearxfr  36288  lineext  36289  fscgr  36293  linecgr  36294  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  seglecgr12im  36323  seglecgr12  36324  segletr  36327  broutsideof3  36339  outsideofeq  36343  lineunray  36360  linecom  36363  eqlkr  39472  lshpkrlem5  39487  omlmod1i2N  39633  cvrnbtwn3  39649  cvrcmp2  39657  cvlexch2  39702  cvlexchb2  39704  cvlatexchb2  39708  cvlatexch1  39709  cvlatexch2  39710  cvlatexch3  39711  cvlsupr7  39721  cvlsupr8  39722  atnlej1  39752  atnlej2  39753  2llnneN  39782  cvratlem  39794  atcvrneN  39803  atlelt  39811  2atjm  39818  3noncolr2  39822  3noncolr1N  39823  hlatcon2  39825  3dimlem2  39832  3dim1  39840  3dim2  39841  1cvrat  39849  ps-1  39850  ps-2  39851  2atjlej  39852  hlatexch3N  39853  ps-2b  39855  3atlem1  39856  3atlem5  39860  3atlem6  39861  2atm  39900  ps-2c  39901  lplni2  39910  lplnri3N  39928  llncvrlpln2  39930  2atmat  39934  2llnm2N  39941  2llnm3N  39942  2llnm4  39943  2llnmeqat  39944  lvolnle3at  39955  4atlem0ae  39967  4atlem0be  39968  4atlem3b  39971  4atlem9  39976  4atlem10a  39977  4atlem10  39979  4atlem11a  39980  4atlem12a  39983  4at2  39987  2lplnm2N  39994  lneq2at  40151  2llnma1b  40159  2llnma1  40160  2llnma3r  40161  2llnma2  40162  2llnma2rN  40163  cdlema1N  40164  paddasslem2  40194  paddasslem16  40208  pmodlem1  40219  pmod2iN  40222  hlmod1i  40229  atmod2i1  40234  atmod2i2  40235  atmod3i1  40237  atmod3i2  40238  atmod4i1  40239  atmod4i2  40240  llnexchb2lem  40241  llnexch2N  40243  dalawlem3  40246  dalawlem4  40247  dalawlem5  40248  dalawlem6  40249  dalawlem7  40250  dalawlem8  40251  dalawlem9  40252  dalawlem11  40254  dalawlem12  40255  dalawlem13  40256  dalawlem15  40258  osumcllem7N  40335  osumcllem9N  40337  pl42lem1N  40352  4atexlemswapqr  40436  4atex2  40450  4atex2-0bOLDN  40452  trlval4  40561  cdlemc5  40568  cdlemc6  40569  cdlemd2  40572  cdlemd4  40574  cdlemd6  40576  cdleme00a  40582  cdleme0e  40590  cdleme4  40611  cdleme4a  40612  cdleme5  40613  cdleme9  40626  cdleme16aN  40632  cdleme11c  40634  cdleme11dN  40635  cdleme11e  40636  cdleme11g  40638  cdleme11h  40639  cdleme11j  40640  cdleme11k  40641  cdleme11l  40642  cdleme11  40643  cdleme12  40644  cdleme13  40645  cdleme14  40646  cdleme15a  40647  cdleme15c  40649  cdleme16b  40652  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme16f  40656  cdleme17d1  40662  cdleme0nex  40663  cdleme18a  40664  cdleme18b  40665  cdleme18c  40666  cdleme18d  40668  cdlemednpq  40672  cdlemednuN  40673  cdleme20zN  40674  cdleme20y  40675  cdleme19a  40676  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20aN  40682  cdleme20d  40685  cdleme20f  40687  cdleme20g  40688  cdleme20i  40690  cdleme20j  40691  cdleme20l1  40693  cdleme20l2  40694  cdleme20l  40695  cdleme20m  40696  cdleme21b  40699  cdleme21c  40700  cdleme21e  40704  cdleme21j  40709  cdleme22aa  40712  cdleme22a  40713  cdleme22b  40714  cdleme22cN  40715  cdleme22d  40716  cdleme22e  40717  cdleme22eALTN  40718  cdleme22f  40719  cdleme26fALTN  40735  cdleme26f  40736  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme27N  40742  cdleme28a  40743  cdleme28b  40744  cdleme30a  40751  cdlemefs31fv1  40797  cdleme32b  40815  cdleme32c  40816  cdleme32e  40818  cdleme35h  40829  cdleme36a  40833  cdleme36m  40834  cdleme41sn3aw  40847  cdleme41sn4aw  40848  cdleme41fva11  40850  cdleme42k  40857  cdleme43cN  40864  cdleme46f2g1  40867  cdlemeg46fjgN  40894  cdlemeg46fjv  40896  cdlemeg46frv  40898  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemeg46gfv  40903  cdleme50trn2a  40923  cdlemg4a  40981  cdlemg4d  40986  cdlemg4e  40987  cdlemg4f  40988  cdlemg8c  41002  cdlemg9a  41005  cdlemg9b  41006  cdlemg10a  41013  cdlemg10  41014  cdlemg12b  41017  cdlemg12f  41021  cdlemg12g  41022  cdlemg12  41023  cdlemg17dN  41036  cdlemg17dALTN  41037  cdlemg17e  41038  cdlemg17f  41039  cdlemg17g  41040  cdlemg17i  41042  cdlemg17ir  41043  cdlemg17pq  41045  cdlemg17bq  41046  cdlemg17iqN  41047  cdlemg17  41050  cdlemg18b  41052  cdlemg18c  41053  cdlemg18d  41054  cdlemg18  41055  cdlemg19  41057  cdlemg21  41059  cdlemg28a  41066  cdlemg31b0a  41068  cdlemg27b  41069  cdlemg33b0  41074  cdlemg28b  41076  cdlemg28  41077  cdlemg35  41086  cdlemg36  41087  cdlemg44a  41104  cdlemh  41190  cdlemi2  41192  cdlemj1  41194  tendocan  41197  cdlemk5a  41208  cdlemk5  41209  cdlemki  41214  cdlemkvcl  41215  cdlemk10  41216  cdlemksv2  41220  cdlemk7  41221  cdlemk11  41222  cdlemk12  41223  cdlemkoatnle  41224  cdlemk15  41228  cdlemk16a  41229  cdlemk16  41230  cdlemk1u  41232  cdlemk5u  41234  cdlemk6u  41235  cdlemk18  41241  cdlemk19  41242  cdlemk7u  41243  cdlemk11u  41244  cdlemk12u  41245  cdlemk21N  41246  cdlemk20  41247  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk22  41266  cdlemk30  41267  cdlemkuel-3  41271  cdlemkuv2-3N  41272  cdlemk18-3N  41273  cdlemkfid1N  41294  cdlemkid1  41295  cdlemkfid3N  41298  cdlemky  41299  cdlemk11ta  41302  cdlemk47  41322  cdlemk48  41323  cdlemk49  41324  cdlemk50  41325  cdlemk51  41326  cdlemk52  41327  cdlemk53a  41328  cdlemk53  41330  cdlemk54  41331  cdlemk55a  41332  cdlemkyyN  41335  cdlemk43N  41336  cdlemk55u1  41338  cdlemk55u  41339  cdlemk39u1  41340  cdlemk19u1  41342  cdleml1N  41349  cdleml2N  41350  cdleml3N  41351  dia2dimlem6  41442  cdlemn2  41568  cdlemn2a  41569  cdlemn5pre  41573  cdlemn11a  41580  dihjustlem  41589  dihjust  41590  dihmeetlem15N  41694  lclkrlem2y  41904  aks6d1c1  42483  relexpmulnn  44062  ormkglobd  47230  natglobalincr  47232  iscnrm3llem1  49305  iscnrm3l  49307  swapffunc  49638  fucofunc  49715  amgmwlem  50158