Theorem simp23 1227

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 1156	. 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:  simp123  1326  simp223  1335  simp323  1344  omeulem1  8569  elfiun  9400  ttrclselem2  9705  cofsmo  10271  modexp  14302  iscatd2  17769  funcoppc  17964  funcres  17985  catcisolem  18199  1stfcl  18285  2ndfcl  18286  prfcl  18291  evlfcl  18310  curf1cl  18316  curfcl  18320  hofcl  18347  pmtrprfv3  19581  ogrpsub  20264  ogrpsublt  20269  mdetunilem3  22836  mdetunilem4  22837  mdetuni0  22843  mdetmul  22845  prdsxmetlem  24594  isosctrlem3  27057  isosctr  27058  noinfbnd2lem1  27966  addsass  28270  f1otrg  29327  colinearalg  29367  ax5seglem6  29391  ax5seg  29395  axpasch  29398  axeuclid  29420  uhgr2edg  29668  clwwlkccat  30460  rhmdvd  33764  bnj966  35453  bnj967  35454  mclspps  36163  cgrtr  36572  cgrtr3  36574  ofscom  36587  btwnxfr  36636  colinearxfr  36655  lineext  36656  brofs2  36657  brifs2  36658  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  eqlkr  39972  omlmod1i2N  40133  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  atcvrj1  40304  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  3atlem2  40357  3atlem6  40361  llnle  40391  2atm  40400  ps-2c  40401  lplni2  40410  lplnle  40413  lplnnle2at  40414  lplnri3N  40428  llncvrlpln2  40430  2atmat  40434  2llnjaN  40439  2llnm2N  40441  2llnm4  40443  2llnmeqat  40444  lvolnle3at  40455  4atlem0ae  40467  4atlem0be  40468  4atlem3b  40471  4atlem9  40476  4atlem10a  40477  4atlem10  40479  4atlem11a  40480  4atlem12a  40483  4at  40486  4at2  40487  lplncvrlvol2  40488  2lplnm2N  40494  2llnma1b  40659  2llnma1  40660  2llnma3r  40661  2llnma2  40662  2llnma2rN  40663  cdlema1N  40664  cdlema2N  40665  paddasslem2  40694  paddasslem15  40707  paddasslem16  40708  pmodlem1  40719  pmod2iN  40722  hlmod1i  40729  atmod2i1  40734  atmod2i2  40735  atmod3i1  40737  atmod3i2  40738  atmod4i1  40739  atmod4i2  40740  llnexchb2  40742  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem13  40756  dalawlem15  40758  osumcllem7N  40835  osumcllem9N  40837  osumcllem11N  40839  pl42lem1N  40852  4atex  40949  4atex2-0aOLDN  40951  4atex2-0bOLDN  40952  4atex2-0cOLDN  40953  trlval4  41061  cdlemc5  41068  cdlemd5  41075  cdlemd6  41076  cdleme00a  41082  cdleme3g  41107  cdleme3h  41108  cdleme3  41110  cdleme4  41111  cdleme4a  41112  cdleme16aN  41132  cdleme11c  41134  cdleme11g  41138  cdleme11h  41139  cdleme12  41144  cdleme0nex  41163  cdleme18a  41164  cdleme18b  41165  cdleme18c  41166  cdleme18d  41168  cdleme20zN  41174  cdleme20y  41175  cdleme19a  41176  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20aN  41182  cdleme20c  41184  cdleme20d  41185  cdleme20i  41190  cdleme20j  41191  cdleme20l1  41193  cdleme20l2  41194  cdleme20m  41196  cdleme21b  41199  cdleme21c  41200  cdleme21j  41209  cdleme22aa  41212  cdleme22a  41213  cdleme22eALTN  41218  cdleme26e  41232  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme27N  41242  cdleme28a  41243  cdleme28b  41244  cdleme30a  41251  cdlemefs45eN  41304  cdleme32c  41316  cdleme32e  41318  cdleme35h  41329  cdleme36a  41333  cdleme36m  41334  cdleme37m  41335  cdleme41sn3aw  41347  cdleme41sn4aw  41348  cdleme41fva11  41350  cdleme42k  41357  cdleme43cN  41364  cdleme43dN  41365  cdleme46f2g1  41367  cdlemeg47rv2  41383  cdlemeg46sfg  41393  cdlemeg46fjgN  41394  cdlemeg46rjgN  41395  cdlemeg46fjv  41396  cdlemeg46frv  41398  cdlemeg46vrg  41400  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemeg46gfv  41403  cdleme50trn2a  41423  cdlemg2fv2  41473  cdlemg4a  41481  cdlemg4e  41487  cdlemg4f  41488  cdlemg8b  41501  cdlemg8c  41502  cdlemg9a  41505  cdlemg9b  41506  cdlemg9  41507  cdlemg10a  41513  cdlemg12a  41516  cdlemg12b  41517  cdlemg12c  41518  cdlemg12  41523  cdlemg17dN  41536  cdlemg17dALTN  41537  cdlemg17e  41538  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  cdlemg33b0  41574  cdlemg35  41586  cdlemg44a  41604  cdlemh  41690  cdlemi2  41692  cdlemj1  41694  cdlemk5a  41708  cdlemk5  41709  cdlemki  41714  cdlemkvcl  41715  cdlemk10  41716  cdlemksv2  41720  cdlemk7  41721  cdlemk11  41722  cdlemk12  41723  cdlemk15  41728  cdlemk16a  41729  cdlemk16  41730  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  cdlemk28-3  41781  cdlemk33N  41782  cdlemkfid1N  41794  cdlemkid1  41795  cdlemky  41799  cdlemk11ta  41802  cdlemk35s-id  41811  cdlemk39s-id  41813  cdlemk47  41822  cdlemk48  41823  cdlemk49  41824  cdlemk50  41825  cdlemk51  41826  cdlemk52  41827  cdlemk53a  41828  cdlemk53b  41829  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  cdlemn11pre  42083  dihjustlem  42089  dihjust  42090  dihmeetlem15N  42194  lclkrlem2y  42404  relexpxpnnidm  44543  ormkglobd  47705  iscnrm3llem1  49875  iscnrm3l  49877  swapffunc  50208  fucofunc  50285