Theorem simp23 1209

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp23	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃)

Proof of Theorem simp23

Step	Hyp	Ref	Expression
1		simp3 1138	. 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:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8592  elfiun  9440  ttrclselem2  9738  cofsmo  10281  modexp  14254  iscatd2  17691  funcoppc  17886  funcres  17907  catcisolem  18121  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlfcl  18232  curf1cl  18238  curfcl  18242  hofcl  18269  pmtrprfv3  19433  mdetunilem3  22550  mdetunilem4  22551  mdetuni0  22557  mdetmul  22559  prdsxmetlem  24305  isosctrlem3  26780  isosctr  26781  noinfbnd2lem1  27692  addsass  27955  f1otrg  28796  colinearalg  28835  ax5seglem6  28859  ax5seg  28863  axpasch  28866  axeuclid  28888  uhgr2edg  29133  clwwlkccat  29917  ogrpsub  33030  ogrpsublt  33035  rhmdvd  33286  bnj966  34921  bnj967  34922  mclspps  35552  cgrtr  35956  cgrtr3  35958  ofscom  35971  btwnxfr  36020  colinearxfr  36039  lineext  36040  brofs2  36041  brifs2  36042  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  eqlkr  39063  omlmod1i2N  39224  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  atcvrj1  39396  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  3atlem2  39449  3atlem6  39453  llnle  39483  2atm  39492  ps-2c  39493  lplni2  39502  lplnle  39505  lplnnle2at  39506  lplnri3N  39520  llncvrlpln2  39522  2atmat  39526  2llnjaN  39531  2llnm2N  39533  2llnm4  39535  2llnmeqat  39536  lvolnle3at  39547  4atlem0ae  39559  4atlem0be  39560  4atlem3b  39563  4atlem9  39568  4atlem10a  39569  4atlem10  39571  4atlem11a  39572  4atlem12a  39575  4at  39578  4at2  39579  lplncvrlvol2  39580  2lplnm2N  39586  2llnma1b  39751  2llnma1  39752  2llnma3r  39753  2llnma2  39754  2llnma2rN  39755  cdlema1N  39756  cdlema2N  39757  paddasslem2  39786  paddasslem15  39799  paddasslem16  39800  pmodlem1  39811  pmod2iN  39814  hlmod1i  39821  atmod2i1  39826  atmod2i2  39827  atmod3i1  39829  atmod3i2  39830  atmod4i1  39831  atmod4i2  39832  llnexchb2  39834  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem13  39848  dalawlem15  39850  osumcllem7N  39927  osumcllem9N  39929  osumcllem11N  39931  pl42lem1N  39944  4atex  40041  4atex2-0aOLDN  40043  4atex2-0bOLDN  40044  4atex2-0cOLDN  40045  trlval4  40153  cdlemc5  40160  cdlemd5  40167  cdlemd6  40168  cdleme00a  40174  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme4  40203  cdleme4a  40204  cdleme16aN  40224  cdleme11c  40226  cdleme11g  40230  cdleme11h  40231  cdleme12  40236  cdleme0nex  40255  cdleme18a  40256  cdleme18b  40257  cdleme18c  40258  cdleme18d  40260  cdleme20zN  40266  cdleme20y  40267  cdleme19a  40268  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20aN  40274  cdleme20c  40276  cdleme20d  40277  cdleme20i  40282  cdleme20j  40283  cdleme20l1  40285  cdleme20l2  40286  cdleme20m  40288  cdleme21b  40291  cdleme21c  40292  cdleme21j  40301  cdleme22aa  40304  cdleme22a  40305  cdleme22eALTN  40310  cdleme26e  40324  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme27N  40334  cdleme28a  40335  cdleme28b  40336  cdleme30a  40343  cdlemefs45eN  40396  cdleme32c  40408  cdleme32e  40410  cdleme35h  40421  cdleme36a  40425  cdleme36m  40426  cdleme37m  40427  cdleme41sn3aw  40439  cdleme41sn4aw  40440  cdleme41fva11  40442  cdleme42k  40449  cdleme43cN  40456  cdleme43dN  40457  cdleme46f2g1  40459  cdlemeg47rv2  40475  cdlemeg46sfg  40485  cdlemeg46fjgN  40486  cdlemeg46rjgN  40487  cdlemeg46fjv  40488  cdlemeg46frv  40490  cdlemeg46vrg  40492  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdleme50trn2a  40515  cdlemg2fv2  40565  cdlemg4a  40573  cdlemg4e  40579  cdlemg4f  40580  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg9b  40598  cdlemg9  40599  cdlemg10a  40605  cdlemg12a  40608  cdlemg12b  40609  cdlemg12c  40610  cdlemg12  40615  cdlemg17dN  40628  cdlemg17dALTN  40629  cdlemg17e  40630  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  cdlemg33b0  40666  cdlemg35  40678  cdlemg44a  40696  cdlemh  40782  cdlemi2  40784  cdlemj1  40786  cdlemk5a  40800  cdlemk5  40801  cdlemki  40806  cdlemkvcl  40807  cdlemk10  40808  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  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  cdlemk28-3  40873  cdlemk33N  40874  cdlemkfid1N  40886  cdlemkid1  40887  cdlemky  40891  cdlemk11ta  40894  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk53b  40921  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  cdlemn11pre  41175  dihjustlem  41181  dihjust  41182  dihmeetlem15N  41286  lclkrlem2y  41496  relexpxpnnidm  43674  ormkglobd  46852  natglobalincr  46854  iscnrm3llem1  48871  iscnrm3l  48873  swapffunc  49147  fucofunc  49218