Theorem simp22 1208

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 1086

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 1088

This theorem is referenced by:  simp122  1307  simp222  1316  simp322  1325  elfiun  9440  cofsmo  10281  modexp  14254  funcoppc  17886  funcres  17907  catcisolem  18121  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlfcl  18232  curf1cl  18238  curfcl  18242  hofcl  18269  mulgdirlem  19086  pmtrprfv3  19433  mdetunilem4  22551  mdetuni0  22557  mdetmul  22559  prdsxmetlem  24305  isosctrlem3  26780  isosctr  26781  amgmlem  26950  f1otrg  28796  colinearalg  28835  ax5seglem6  28859  ax5seg  28863  axpasch  28866  axeuclidlem  28887  axeuclid  28888  ogrpsub  33030  ogrpaddlt  33031  ogrpsublt  33035  rhmdvd  33286  bnj966  34921  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  39063  lshpkrlem5  39078  omlmod1i2N  39224  cvrnbtwn3  39240  cvrcmp2  39248  cvlexch2  39293  cvlexchb2  39295  cvlatexchb2  39299  cvlatexch1  39300  cvlatexch2  39301  cvlatexch3  39302  cvlsupr7  39312  cvlsupr8  39313  atnlej1  39344  atnlej2  39345  2llnneN  39374  cvratlem  39386  atcvrneN  39395  atlelt  39403  2atjm  39410  3noncolr2  39414  3noncolr1N  39415  hlatcon2  39417  3dimlem2  39424  3dim1  39432  3dim2  39433  1cvrat  39441  ps-1  39442  ps-2  39443  2atjlej  39444  hlatexch3N  39445  ps-2b  39447  3atlem1  39448  3atlem5  39452  3atlem6  39453  2atm  39492  ps-2c  39493  lplni2  39502  lplnri3N  39520  llncvrlpln2  39522  2atmat  39526  2llnm2N  39533  2llnm3N  39534  2llnm4  39535  2llnmeqat  39536  lvolnle3at  39547  4atlem0ae  39559  4atlem0be  39560  4atlem3b  39563  4atlem9  39568  4atlem10a  39569  4atlem10  39571  4atlem11a  39572  4atlem12a  39575  4at2  39579  2lplnm2N  39586  lneq2at  39743  2llnma1b  39751  2llnma1  39752  2llnma3r  39753  2llnma2  39754  2llnma2rN  39755  cdlema1N  39756  paddasslem2  39786  paddasslem16  39800  pmodlem1  39811  pmod2iN  39814  hlmod1i  39821  atmod2i1  39826  atmod2i2  39827  atmod3i1  39829  atmod3i2  39830  atmod4i1  39831  atmod4i2  39832  llnexchb2lem  39833  llnexch2N  39835  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem13  39848  dalawlem15  39850  osumcllem7N  39927  osumcllem9N  39929  pl42lem1N  39944  4atexlemswapqr  40028  4atex2  40042  4atex2-0bOLDN  40044  trlval4  40153  cdlemc5  40160  cdlemc6  40161  cdlemd2  40164  cdlemd4  40166  cdlemd6  40168  cdleme00a  40174  cdleme0e  40182  cdleme4  40203  cdleme4a  40204  cdleme5  40205  cdleme9  40218  cdleme16aN  40224  cdleme11c  40226  cdleme11dN  40227  cdleme11e  40228  cdleme11g  40230  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme11l  40234  cdleme11  40235  cdleme12  40236  cdleme13  40237  cdleme14  40238  cdleme15a  40239  cdleme15c  40241  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme17d1  40254  cdleme0nex  40255  cdleme18a  40256  cdleme18b  40257  cdleme18c  40258  cdleme18d  40260  cdlemednpq  40264  cdlemednuN  40265  cdleme20zN  40266  cdleme20y  40267  cdleme19a  40268  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20aN  40274  cdleme20d  40277  cdleme20f  40279  cdleme20g  40280  cdleme20i  40282  cdleme20j  40283  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21b  40291  cdleme21c  40292  cdleme21e  40296  cdleme21j  40301  cdleme22aa  40304  cdleme22a  40305  cdleme22b  40306  cdleme22cN  40307  cdleme22d  40308  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme27N  40334  cdleme28a  40335  cdleme28b  40336  cdleme30a  40343  cdlemefs31fv1  40389  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme35h  40421  cdleme36a  40425  cdleme36m  40426  cdleme41sn3aw  40439  cdleme41sn4aw  40440  cdleme41fva11  40442  cdleme42k  40449  cdleme43cN  40456  cdleme46f2g1  40459  cdlemeg46fjgN  40486  cdlemeg46fjv  40488  cdlemeg46frv  40490  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdleme50trn2a  40515  cdlemg4a  40573  cdlemg4d  40578  cdlemg4e  40579  cdlemg4f  40580  cdlemg8c  40594  cdlemg9a  40597  cdlemg9b  40598  cdlemg10a  40605  cdlemg10  40606  cdlemg12b  40609  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg17dN  40628  cdlemg17dALTN  40629  cdlemg17e  40630  cdlemg17f  40631  cdlemg17g  40632  cdlemg17i  40634  cdlemg17ir  40635  cdlemg17pq  40637  cdlemg17bq  40638  cdlemg17iqN  40639  cdlemg17  40642  cdlemg18b  40644  cdlemg18c  40645  cdlemg18d  40646  cdlemg18  40647  cdlemg19  40649  cdlemg21  40651  cdlemg28a  40658  cdlemg31b0a  40660  cdlemg27b  40661  cdlemg33b0  40666  cdlemg28b  40668  cdlemg28  40669  cdlemg35  40678  cdlemg36  40679  cdlemg44a  40696  cdlemh  40782  cdlemi2  40784  cdlemj1  40786  tendocan  40789  cdlemk5a  40800  cdlemk5  40801  cdlemki  40806  cdlemkvcl  40807  cdlemk10  40808  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemkoatnle  40816  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  cdlemk1u  40824  cdlemk5u  40826  cdlemk6u  40827  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk11u  40836  cdlemk12u  40837  cdlemk21N  40838  cdlemk20  40839  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk22  40858  cdlemk30  40859  cdlemkuel-3  40863  cdlemkuv2-3N  40864  cdlemk18-3N  40865  cdlemkfid1N  40886  cdlemkid1  40887  cdlemkfid3N  40890  cdlemky  40891  cdlemk11ta  40894  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk53  40922  cdlemk54  40923  cdlemk55a  40924  cdlemkyyN  40927  cdlemk43N  40928  cdlemk55u1  40930  cdlemk55u  40931  cdlemk39u1  40932  cdlemk19u1  40934  cdleml1N  40941  cdleml2N  40942  cdleml3N  40943  dia2dimlem6  41034  cdlemn2  41160  cdlemn2a  41161  cdlemn5pre  41165  cdlemn11a  41172  dihjustlem  41181  dihjust  41182  dihmeetlem15N  41286  lclkrlem2y  41496  aks6d1c1  42075  relexpmulnn  43680  ormkglobd  46852  natglobalincr  46854  iscnrm3llem1  48871  iscnrm3l  48873  swapffunc  49147  fucofunc  49218  amgmwlem  49614