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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp122  1306  simp222  1315  simp322  1324  elfiun  9424  cofsmo  10263  modexp  14200  funcoppc  17824  funcres  17845  catcisolem  18059  1stfcl  18148  2ndfcl  18149  prfcl  18154  evlfcl  18174  curf1cl  18180  curfcl  18184  hofcl  18211  mulgdirlem  18984  pmtrprfv3  19321  mdetunilem4  22116  mdetuni0  22122  mdetmul  22124  prdsxmetlem  23873  isosctrlem3  26322  isosctr  26323  amgmlem  26491  f1otrg  28119  colinearalg  28165  ax5seglem6  28189  ax5seg  28193  axpasch  28196  axeuclidlem  28217  axeuclid  28218  ogrpsub  32229  ogrpaddlt  32230  ogrpsublt  32234  rhmdvd  32431  bnj966  33950  mclspps  34570  cgrtr  34959  cgrtr3  34961  ofscom  34974  cgrextend  34975  btwnxfr  35023  colinearxfr  35042  lineext  35043  fscgr  35047  linecgr  35048  btwnconn1lem1  35054  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem7  35060  seglecgr12im  35077  seglecgr12  35078  segletr  35081  broutsideof3  35093  outsideofeq  35097  lineunray  35114  linecom  35117  eqlkr  37964  lshpkrlem5  37979  omlmod1i2N  38125  cvrnbtwn3  38141  cvrcmp2  38149  cvlexch2  38194  cvlexchb2  38196  cvlatexchb2  38200  cvlatexch1  38201  cvlatexch2  38202  cvlatexch3  38203  cvlsupr7  38213  cvlsupr8  38214  atnlej1  38245  atnlej2  38246  2llnneN  38275  cvratlem  38287  atcvrneN  38296  atlelt  38304  2atjm  38311  3noncolr2  38315  3noncolr1N  38316  hlatcon2  38318  3dimlem2  38325  3dim1  38333  3dim2  38334  1cvrat  38342  ps-1  38343  ps-2  38344  2atjlej  38345  hlatexch3N  38346  ps-2b  38348  3atlem1  38349  3atlem5  38353  3atlem6  38354  2atm  38393  ps-2c  38394  lplni2  38403  lplnri3N  38421  llncvrlpln2  38423  2atmat  38427  2llnm2N  38434  2llnm3N  38435  2llnm4  38436  2llnmeqat  38437  lvolnle3at  38448  4atlem0ae  38460  4atlem0be  38461  4atlem3b  38464  4atlem9  38469  4atlem10a  38470  4atlem10  38472  4atlem11a  38473  4atlem12a  38476  4at2  38480  2lplnm2N  38487  lneq2at  38644  2llnma1b  38652  2llnma1  38653  2llnma3r  38654  2llnma2  38655  2llnma2rN  38656  cdlema1N  38657  paddasslem2  38687  paddasslem16  38701  pmodlem1  38712  pmod2iN  38715  hlmod1i  38722  atmod2i1  38727  atmod2i2  38728  atmod3i1  38730  atmod3i2  38731  atmod4i1  38732  atmod4i2  38733  llnexchb2lem  38734  llnexch2N  38736  dalawlem3  38739  dalawlem4  38740  dalawlem5  38741  dalawlem6  38742  dalawlem7  38743  dalawlem8  38744  dalawlem9  38745  dalawlem11  38747  dalawlem12  38748  dalawlem13  38749  dalawlem15  38751  osumcllem7N  38828  osumcllem9N  38830  pl42lem1N  38845  4atexlemswapqr  38929  4atex2  38943  4atex2-0bOLDN  38945  trlval4  39054  cdlemc5  39061  cdlemc6  39062  cdlemd2  39065  cdlemd4  39067  cdlemd6  39069  cdleme00a  39075  cdleme0e  39083  cdleme4  39104  cdleme4a  39105  cdleme5  39106  cdleme9  39119  cdleme16aN  39125  cdleme11c  39127  cdleme11dN  39128  cdleme11e  39129  cdleme11g  39131  cdleme11h  39132  cdleme11j  39133  cdleme11k  39134  cdleme11l  39135  cdleme11  39136  cdleme12  39137  cdleme13  39138  cdleme14  39139  cdleme15a  39140  cdleme15c  39142  cdleme16b  39145  cdleme16c  39146  cdleme16d  39147  cdleme16e  39148  cdleme16f  39149  cdleme17d1  39155  cdleme0nex  39156  cdleme18a  39157  cdleme18b  39158  cdleme18c  39159  cdleme18d  39161  cdlemednpq  39165  cdlemednuN  39166  cdleme20zN  39167  cdleme20y  39168  cdleme19a  39169  cdleme19b  39170  cdleme19d  39172  cdleme19e  39173  cdleme20aN  39175  cdleme20d  39178  cdleme20f  39180  cdleme20g  39181  cdleme20i  39183  cdleme20j  39184  cdleme20l1  39186  cdleme20l2  39187  cdleme20l  39188  cdleme20m  39189  cdleme21b  39192  cdleme21c  39193  cdleme21e  39197  cdleme21j  39202  cdleme22aa  39205  cdleme22a  39206  cdleme22b  39207  cdleme22cN  39208  cdleme22d  39209  cdleme22e  39210  cdleme22eALTN  39211  cdleme22f  39212  cdleme26fALTN  39228  cdleme26f  39229  cdleme26f2ALTN  39230  cdleme26f2  39231  cdleme27N  39235  cdleme28a  39236  cdleme28b  39237  cdleme30a  39244  cdlemefs31fv1  39290  cdleme32b  39308  cdleme32c  39309  cdleme32e  39311  cdleme35h  39322  cdleme36a  39326  cdleme36m  39327  cdleme41sn3aw  39340  cdleme41sn4aw  39341  cdleme41fva11  39343  cdleme42k  39350  cdleme43cN  39357  cdleme46f2g1  39360  cdlemeg46fjgN  39387  cdlemeg46fjv  39389  cdlemeg46frv  39391  cdlemeg46rgv  39394  cdlemeg46req  39395  cdlemeg46gfv  39396  cdleme50trn2a  39416  cdlemg4a  39474  cdlemg4d  39479  cdlemg4e  39480  cdlemg4f  39481  cdlemg8c  39495  cdlemg9a  39498  cdlemg9b  39499  cdlemg10a  39506  cdlemg10  39507  cdlemg12b  39510  cdlemg12f  39514  cdlemg12g  39515  cdlemg12  39516  cdlemg17dN  39529  cdlemg17dALTN  39530  cdlemg17e  39531  cdlemg17f  39532  cdlemg17g  39533  cdlemg17i  39535  cdlemg17ir  39536  cdlemg17pq  39538  cdlemg17bq  39539  cdlemg17iqN  39540  cdlemg17  39543  cdlemg18b  39545  cdlemg18c  39546  cdlemg18d  39547  cdlemg18  39548  cdlemg19  39550  cdlemg21  39552  cdlemg28a  39559  cdlemg31b0a  39561  cdlemg27b  39562  cdlemg33b0  39567  cdlemg28b  39569  cdlemg28  39570  cdlemg35  39579  cdlemg36  39580  cdlemg44a  39597  cdlemh  39683  cdlemi2  39685  cdlemj1  39687  tendocan  39690  cdlemk5a  39701  cdlemk5  39702  cdlemki  39707  cdlemkvcl  39708  cdlemk10  39709  cdlemksv2  39713  cdlemk7  39714  cdlemk11  39715  cdlemk12  39716  cdlemkoatnle  39717  cdlemk15  39721  cdlemk16a  39722  cdlemk16  39723  cdlemk1u  39725  cdlemk5u  39727  cdlemk6u  39728  cdlemk18  39734  cdlemk19  39735  cdlemk7u  39736  cdlemk11u  39737  cdlemk12u  39738  cdlemk21N  39739  cdlemk20  39740  cdlemkoatnle-2N  39741  cdlemk13-2N  39742  cdlemkole-2N  39743  cdlemk14-2N  39744  cdlemk15-2N  39745  cdlemk16-2N  39746  cdlemk17-2N  39747  cdlemk18-2N  39752  cdlemk19-2N  39753  cdlemk22  39759  cdlemk30  39760  cdlemkuel-3  39764  cdlemkuv2-3N  39765  cdlemk18-3N  39766  cdlemkfid1N  39787  cdlemkid1  39788  cdlemkfid3N  39791  cdlemky  39792  cdlemk11ta  39795  cdlemk47  39815  cdlemk48  39816  cdlemk49  39817  cdlemk50  39818  cdlemk51  39819  cdlemk52  39820  cdlemk53a  39821  cdlemk53  39823  cdlemk54  39824  cdlemk55a  39825  cdlemkyyN  39828  cdlemk43N  39829  cdlemk55u1  39831  cdlemk55u  39832  cdlemk39u1  39833  cdlemk19u1  39835  cdleml1N  39842  cdleml2N  39843  cdleml3N  39844  dia2dimlem6  39935  cdlemn2  40061  cdlemn2a  40062  cdlemn5pre  40066  cdlemn11a  40073  dihjustlem  40082  dihjust  40083  dihmeetlem15N  40187  lclkrlem2y  40397  relexpmulnn  42450  natglobalincr  45581  iscnrm3llem1  47572  iscnrm3l  47574  amgmwlem  47839