Theorem simp22 1226

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp122  1325  simp222  1334  simp322  1343  elfiun  9400  cofsmo  10271  modexp  14302  funcoppc  17964  funcres  17985  catcisolem  18199  1stfcl  18285  2ndfcl  18286  prfcl  18291  evlfcl  18310  curf1cl  18316  curfcl  18320  hofcl  18347  mulgdirlem  19228  pmtrprfv3  19581  ogrpsub  20264  ogrpaddlt  20265  ogrpsublt  20269  mdetunilem4  22837  mdetuni0  22843  mdetmul  22845  prdsxmetlem  24594  isosctrlem3  27057  isosctr  27058  amgmlem  27226  f1otrg  29327  colinearalg  29367  ax5seglem6  29391  ax5seg  29395  axpasch  29398  axeuclidlem  29419  axeuclid  29420  rhmdvd  33764  bnj966  35453  mclspps  36163  cgrtr  36572  cgrtr3  36574  ofscom  36587  cgrextend  36588  btwnxfr  36636  colinearxfr  36655  lineext  36656  fscgr  36660  linecgr  36661  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem3  36669  btwnconn1lem4  36670  btwnconn1lem5  36671  btwnconn1lem6  36672  btwnconn1lem7  36673  seglecgr12im  36690  seglecgr12  36691  segletr  36694  broutsideof3  36706  outsideofeq  36710  lineunray  36727  linecom  36730  eqlkr  39972  lshpkrlem5  39987  omlmod1i2N  40133  cvrnbtwn3  40149  cvrcmp2  40157  cvlexch2  40202  cvlexchb2  40204  cvlatexchb2  40208  cvlatexch1  40209  cvlatexch2  40210  cvlatexch3  40211  cvlsupr7  40221  cvlsupr8  40222  atnlej1  40252  atnlej2  40253  2llnneN  40282  cvratlem  40294  atcvrneN  40303  atlelt  40311  2atjm  40318  3noncolr2  40322  3noncolr1N  40323  hlatcon2  40325  3dimlem2  40332  3dim1  40340  3dim2  40341  1cvrat  40349  ps-1  40350  ps-2  40351  2atjlej  40352  hlatexch3N  40353  ps-2b  40355  3atlem1  40356  3atlem5  40360  3atlem6  40361  2atm  40400  ps-2c  40401  lplni2  40410  lplnri3N  40428  llncvrlpln2  40430  2atmat  40434  2llnm2N  40441  2llnm3N  40442  2llnm4  40443  2llnmeqat  40444  lvolnle3at  40455  4atlem0ae  40467  4atlem0be  40468  4atlem3b  40471  4atlem9  40476  4atlem10a  40477  4atlem10  40479  4atlem11a  40480  4atlem12a  40483  4at2  40487  2lplnm2N  40494  lneq2at  40651  2llnma1b  40659  2llnma1  40660  2llnma3r  40661  2llnma2  40662  2llnma2rN  40663  cdlema1N  40664  paddasslem2  40694  paddasslem16  40708  pmodlem1  40719  pmod2iN  40722  hlmod1i  40729  atmod2i1  40734  atmod2i2  40735  atmod3i1  40737  atmod3i2  40738  atmod4i1  40739  atmod4i2  40740  llnexchb2lem  40741  llnexch2N  40743  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem13  40756  dalawlem15  40758  osumcllem7N  40835  osumcllem9N  40837  pl42lem1N  40852  4atexlemswapqr  40936  4atex2  40950  4atex2-0bOLDN  40952  trlval4  41061  cdlemc5  41068  cdlemc6  41069  cdlemd2  41072  cdlemd4  41074  cdlemd6  41076  cdleme00a  41082  cdleme0e  41090  cdleme4  41111  cdleme4a  41112  cdleme5  41113  cdleme9  41126  cdleme16aN  41132  cdleme11c  41134  cdleme11dN  41135  cdleme11e  41136  cdleme11g  41138  cdleme11h  41139  cdleme11j  41140  cdleme11k  41141  cdleme11l  41142  cdleme11  41143  cdleme12  41144  cdleme13  41145  cdleme14  41146  cdleme15a  41147  cdleme15c  41149  cdleme16b  41152  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme17d1  41162  cdleme0nex  41163  cdleme18a  41164  cdleme18b  41165  cdleme18c  41166  cdleme18d  41168  cdlemednpq  41172  cdlemednuN  41173  cdleme20zN  41174  cdleme20y  41175  cdleme19a  41176  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20aN  41182  cdleme20d  41185  cdleme20f  41187  cdleme20g  41188  cdleme20i  41190  cdleme20j  41191  cdleme20l1  41193  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme21b  41199  cdleme21c  41200  cdleme21e  41204  cdleme21j  41209  cdleme22aa  41212  cdleme22a  41213  cdleme22b  41214  cdleme22cN  41215  cdleme22d  41216  cdleme22e  41217  cdleme22eALTN  41218  cdleme22f  41219  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme27N  41242  cdleme28a  41243  cdleme28b  41244  cdleme30a  41251  cdlemefs31fv1  41297  cdleme32b  41315  cdleme32c  41316  cdleme32e  41318  cdleme35h  41329  cdleme36a  41333  cdleme36m  41334  cdleme41sn3aw  41347  cdleme41sn4aw  41348  cdleme41fva11  41350  cdleme42k  41357  cdleme43cN  41364  cdleme46f2g1  41367  cdlemeg46fjgN  41394  cdlemeg46fjv  41396  cdlemeg46frv  41398  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemeg46gfv  41403  cdleme50trn2a  41423  cdlemg4a  41481  cdlemg4d  41486  cdlemg4e  41487  cdlemg4f  41488  cdlemg8c  41502  cdlemg9a  41505  cdlemg9b  41506  cdlemg10a  41513  cdlemg10  41514  cdlemg12b  41517  cdlemg12f  41521  cdlemg12g  41522  cdlemg12  41523  cdlemg17dN  41536  cdlemg17dALTN  41537  cdlemg17e  41538  cdlemg17f  41539  cdlemg17g  41540  cdlemg17i  41542  cdlemg17ir  41543  cdlemg17pq  41545  cdlemg17bq  41546  cdlemg17iqN  41547  cdlemg17  41550  cdlemg18b  41552  cdlemg18c  41553  cdlemg18d  41554  cdlemg18  41555  cdlemg19  41557  cdlemg21  41559  cdlemg28a  41566  cdlemg31b0a  41568  cdlemg27b  41569  cdlemg33b0  41574  cdlemg28b  41576  cdlemg28  41577  cdlemg35  41586  cdlemg36  41587  cdlemg44a  41604  cdlemh  41690  cdlemi2  41692  cdlemj1  41694  tendocan  41697  cdlemk5a  41708  cdlemk5  41709  cdlemki  41714  cdlemkvcl  41715  cdlemk10  41716  cdlemksv2  41720  cdlemk7  41721  cdlemk11  41722  cdlemk12  41723  cdlemkoatnle  41724  cdlemk15  41728  cdlemk16a  41729  cdlemk16  41730  cdlemk1u  41732  cdlemk5u  41734  cdlemk6u  41735  cdlemk18  41741  cdlemk19  41742  cdlemk7u  41743  cdlemk11u  41744  cdlemk12u  41745  cdlemk21N  41746  cdlemk20  41747  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk22  41766  cdlemk30  41767  cdlemkuel-3  41771  cdlemkuv2-3N  41772  cdlemk18-3N  41773  cdlemkfid1N  41794  cdlemkid1  41795  cdlemkfid3N  41798  cdlemky  41799  cdlemk11ta  41802  cdlemk47  41822  cdlemk48  41823  cdlemk49  41824  cdlemk50  41825  cdlemk51  41826  cdlemk52  41827  cdlemk53a  41828  cdlemk53  41830  cdlemk54  41831  cdlemk55a  41832  cdlemkyyN  41835  cdlemk43N  41836  cdlemk55u1  41838  cdlemk55u  41839  cdlemk39u1  41840  cdlemk19u1  41842  cdleml1N  41849  cdleml2N  41850  cdleml3N  41851  dia2dimlem6  41942  cdlemn2  42068  cdlemn2a  42069  cdlemn5pre  42073  cdlemn11a  42080  dihjustlem  42089  dihjust  42090  dihmeetlem15N  42194  lclkrlem2y  42404  aks6d1c1  42982  relexpmulnn  44549  ormkglobd  47705  iscnrm3llem1  49875  iscnrm3l  49877  swapffunc  50208  fucofunc  50285  amgmwlem  50820