Theorem simp22 1214

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp122  1313  simp222  1322  simp322  1331  elfiun  9333  cofsmo  10182  modexp  14191  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  mulgdirlem  19072  pmtrprfv3  19420  ogrpsub  20103  ogrpaddlt  20104  ogrpsublt  20108  mdetunilem4  22598  mdetuni0  22604  mdetmul  22606  prdsxmetlem  24351  isosctrlem3  26802  isosctr  26803  amgmlem  26971  f1otrg  28957  colinearalg  28997  ax5seglem6  29021  ax5seg  29025  axpasch  29028  axeuclidlem  29049  axeuclid  29050  rhmdvd  33407  bnj966  35126  mclspps  35812  cgrtr  36220  cgrtr3  36222  ofscom  36235  cgrextend  36236  btwnxfr  36284  colinearxfr  36303  lineext  36304  fscgr  36308  linecgr  36309  btwnconn1lem1  36315  btwnconn1lem2  36316  btwnconn1lem3  36317  btwnconn1lem4  36318  btwnconn1lem5  36319  btwnconn1lem6  36320  btwnconn1lem7  36321  seglecgr12im  36338  seglecgr12  36339  segletr  36342  broutsideof3  36354  outsideofeq  36358  lineunray  36375  linecom  36378  eqlkr  39591  lshpkrlem5  39606  omlmod1i2N  39752  cvrnbtwn3  39768  cvrcmp2  39776  cvlexch2  39821  cvlexchb2  39823  cvlatexchb2  39827  cvlatexch1  39828  cvlatexch2  39829  cvlatexch3  39830  cvlsupr7  39840  cvlsupr8  39841  atnlej1  39871  atnlej2  39872  2llnneN  39901  cvratlem  39913  atcvrneN  39922  atlelt  39930  2atjm  39937  3noncolr2  39941  3noncolr1N  39942  hlatcon2  39944  3dimlem2  39951  3dim1  39959  3dim2  39960  1cvrat  39968  ps-1  39969  ps-2  39970  2atjlej  39971  hlatexch3N  39972  ps-2b  39974  3atlem1  39975  3atlem5  39979  3atlem6  39980  2atm  40019  ps-2c  40020  lplni2  40029  lplnri3N  40047  llncvrlpln2  40049  2atmat  40053  2llnm2N  40060  2llnm3N  40061  2llnm4  40062  2llnmeqat  40063  lvolnle3at  40074  4atlem0ae  40086  4atlem0be  40087  4atlem3b  40090  4atlem9  40095  4atlem10a  40096  4atlem10  40098  4atlem11a  40099  4atlem12a  40102  4at2  40106  2lplnm2N  40113  lneq2at  40270  2llnma1b  40278  2llnma1  40279  2llnma3r  40280  2llnma2  40281  2llnma2rN  40282  cdlema1N  40283  paddasslem2  40313  paddasslem16  40327  pmodlem1  40338  pmod2iN  40341  hlmod1i  40348  atmod2i1  40353  atmod2i2  40354  atmod3i1  40356  atmod3i2  40357  atmod4i1  40358  atmod4i2  40359  llnexchb2lem  40360  llnexch2N  40362  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem13  40375  dalawlem15  40377  osumcllem7N  40454  osumcllem9N  40456  pl42lem1N  40471  4atexlemswapqr  40555  4atex2  40569  4atex2-0bOLDN  40571  trlval4  40680  cdlemc5  40687  cdlemc6  40688  cdlemd2  40691  cdlemd4  40693  cdlemd6  40695  cdleme00a  40701  cdleme0e  40709  cdleme4  40730  cdleme4a  40731  cdleme5  40732  cdleme9  40745  cdleme16aN  40751  cdleme11c  40753  cdleme11dN  40754  cdleme11e  40755  cdleme11g  40757  cdleme11h  40758  cdleme11j  40759  cdleme11k  40760  cdleme11l  40761  cdleme11  40762  cdleme12  40763  cdleme13  40764  cdleme14  40765  cdleme15a  40766  cdleme15c  40768  cdleme16b  40771  cdleme16c  40772  cdleme16d  40773  cdleme16e  40774  cdleme16f  40775  cdleme17d1  40781  cdleme0nex  40782  cdleme18a  40783  cdleme18b  40784  cdleme18c  40785  cdleme18d  40787  cdlemednpq  40791  cdlemednuN  40792  cdleme20zN  40793  cdleme20y  40794  cdleme19a  40795  cdleme19b  40796  cdleme19d  40798  cdleme19e  40799  cdleme20aN  40801  cdleme20d  40804  cdleme20f  40806  cdleme20g  40807  cdleme20i  40809  cdleme20j  40810  cdleme20l1  40812  cdleme20l2  40813  cdleme20l  40814  cdleme20m  40815  cdleme21b  40818  cdleme21c  40819  cdleme21e  40823  cdleme21j  40828  cdleme22aa  40831  cdleme22a  40832  cdleme22b  40833  cdleme22cN  40834  cdleme22d  40835  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f  40838  cdleme26fALTN  40854  cdleme26f  40855  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme27N  40861  cdleme28a  40862  cdleme28b  40863  cdleme30a  40870  cdlemefs31fv1  40916  cdleme32b  40934  cdleme32c  40935  cdleme32e  40937  cdleme35h  40948  cdleme36a  40952  cdleme36m  40953  cdleme41sn3aw  40966  cdleme41sn4aw  40967  cdleme41fva11  40969  cdleme42k  40976  cdleme43cN  40983  cdleme46f2g1  40986  cdlemeg46fjgN  41013  cdlemeg46fjv  41015  cdlemeg46frv  41017  cdlemeg46rgv  41020  cdlemeg46req  41021  cdlemeg46gfv  41022  cdleme50trn2a  41042  cdlemg4a  41100  cdlemg4d  41105  cdlemg4e  41106  cdlemg4f  41107  cdlemg8c  41121  cdlemg9a  41124  cdlemg9b  41125  cdlemg10a  41132  cdlemg10  41133  cdlemg12b  41136  cdlemg12f  41140  cdlemg12g  41141  cdlemg12  41142  cdlemg17dN  41155  cdlemg17dALTN  41156  cdlemg17e  41157  cdlemg17f  41158  cdlemg17g  41159  cdlemg17i  41161  cdlemg17ir  41162  cdlemg17pq  41164  cdlemg17bq  41165  cdlemg17iqN  41166  cdlemg17  41169  cdlemg18b  41171  cdlemg18c  41172  cdlemg18d  41173  cdlemg18  41174  cdlemg19  41176  cdlemg21  41178  cdlemg28a  41185  cdlemg31b0a  41187  cdlemg27b  41188  cdlemg33b0  41193  cdlemg28b  41195  cdlemg28  41196  cdlemg35  41205  cdlemg36  41206  cdlemg44a  41223  cdlemh  41309  cdlemi2  41311  cdlemj1  41313  tendocan  41316  cdlemk5a  41327  cdlemk5  41328  cdlemki  41333  cdlemkvcl  41334  cdlemk10  41335  cdlemksv2  41339  cdlemk7  41340  cdlemk11  41341  cdlemk12  41342  cdlemkoatnle  41343  cdlemk15  41347  cdlemk16a  41348  cdlemk16  41349  cdlemk1u  41351  cdlemk5u  41353  cdlemk6u  41354  cdlemk18  41360  cdlemk19  41361  cdlemk7u  41362  cdlemk11u  41363  cdlemk12u  41364  cdlemk21N  41365  cdlemk20  41366  cdlemkoatnle-2N  41367  cdlemk13-2N  41368  cdlemkole-2N  41369  cdlemk14-2N  41370  cdlemk15-2N  41371  cdlemk16-2N  41372  cdlemk17-2N  41373  cdlemk18-2N  41378  cdlemk19-2N  41379  cdlemk22  41385  cdlemk30  41386  cdlemkuel-3  41390  cdlemkuv2-3N  41391  cdlemk18-3N  41392  cdlemkfid1N  41413  cdlemkid1  41414  cdlemkfid3N  41417  cdlemky  41418  cdlemk11ta  41421  cdlemk47  41441  cdlemk48  41442  cdlemk49  41443  cdlemk50  41444  cdlemk51  41445  cdlemk52  41446  cdlemk53a  41447  cdlemk53  41449  cdlemk54  41450  cdlemk55a  41451  cdlemkyyN  41454  cdlemk43N  41455  cdlemk55u1  41457  cdlemk55u  41458  cdlemk39u1  41459  cdlemk19u1  41461  cdleml1N  41468  cdleml2N  41469  cdleml3N  41470  dia2dimlem6  41561  cdlemn2  41687  cdlemn2a  41688  cdlemn5pre  41692  cdlemn11a  41699  dihjustlem  41708  dihjust  41709  dihmeetlem15N  41813  lclkrlem2y  42023  aks6d1c1  42601  relexpmulnn  44153  ormkglobd  47320  natglobalincr  47322  iscnrm3llem1  49439  iscnrm3l  49441  swapffunc  49772  fucofunc  49849  amgmwlem  50292