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  8590  elfiun  9422  ttrclselem2  9727  cofsmo  10347  modexp  14382  iscatd2  17855  funcoppc  18050  funcres  18071  catcisolem  18285  1stfcl  18371  2ndfcl  18372  prfcl  18377  evlfcl  18396  curf1cl  18402  curfcl  18406  hofcl  18433  pmtrprfv3  19668  ogrpsub  20351  ogrpsublt  20356  mdetunilem3  22929  mdetunilem4  22930  mdetuni0  22936  mdetmul  22938  prdsxmetlem  24687  isosctrlem3  27148  isosctr  27149  noinfbnd2lem1  28087  addsass  28391  f1otrg  29448  colinearalg  29488  ax5seglem6  29512  ax5seg  29516  axpasch  29519  axeuclid  29541  uhgr2edg  29789  clwwlkccat  30581  rhmdvd  33885  bnj966  35574  bnj967  35575  mclspps  36349  cgrtr  36757  cgrtr3  36759  ofscom  36772  btwnxfr  36821  colinearxfr  36840  lineext  36841  brofs2  36842  brifs2  36843  fscgr  36845  linecgr  36846  btwnconn1lem1  36852  btwnconn1lem2  36853  btwnconn1lem3  36854  btwnconn1lem4  36855  btwnconn1lem5  36856  btwnconn1lem6  36857  btwnconn1lem7  36858  seglecgr12im  36875  seglecgr12  36876  segletr  36879  broutsideof3  36891  outsideofeq  36895  lineunray  36912  eqlkr  40157  omlmod1i2N  40318  cvrcmp2  40342  cvlexch2  40387  cvlexchb2  40389  cvlatexchb2  40393  cvlatexch1  40394  cvlatexch2  40395  cvlatexch3  40396  cvlsupr7  40406  cvlsupr8  40407  atnlej1  40437  atnlej2  40438  2llnneN  40467  cvratlem  40479  atcvrneN  40488  atcvrj1  40489  atlelt  40496  2atjm  40503  3noncolr2  40507  3noncolr1N  40508  hlatcon2  40510  3dimlem2  40517  3dim1  40525  3dim2  40526  1cvrat  40534  ps-1  40535  ps-2  40536  2atjlej  40537  hlatexch3N  40538  ps-2b  40540  3atlem1  40541  3atlem2  40542  3atlem6  40546  llnle  40576  2atm  40585  ps-2c  40586  lplni2  40595  lplnle  40598  lplnnle2at  40599  lplnri3N  40613  llncvrlpln2  40615  2atmat  40619  2llnjaN  40624  2llnm2N  40626  2llnm4  40628  2llnmeqat  40629  lvolnle3at  40640  4atlem0ae  40652  4atlem0be  40653  4atlem3b  40656  4atlem9  40661  4atlem10a  40662  4atlem10  40664  4atlem11a  40665  4atlem12a  40668  4at  40671  4at2  40672  lplncvrlvol2  40673  2lplnm2N  40679  2llnma1b  40844  2llnma1  40845  2llnma3r  40846  2llnma2  40847  2llnma2rN  40848  cdlema1N  40849  cdlema2N  40850  paddasslem2  40879  paddasslem15  40892  paddasslem16  40893  pmodlem1  40904  pmod2iN  40907  hlmod1i  40914  atmod2i1  40919  atmod2i2  40920  atmod3i1  40922  atmod3i2  40923  atmod4i1  40924  atmod4i2  40925  llnexchb2  40927  dalawlem3  40931  dalawlem4  40932  dalawlem5  40933  dalawlem6  40934  dalawlem7  40935  dalawlem8  40936  dalawlem9  40937  dalawlem11  40939  dalawlem13  40941  dalawlem15  40943  osumcllem7N  41020  osumcllem9N  41022  osumcllem11N  41024  pl42lem1N  41037  4atex  41134  4atex2-0aOLDN  41136  4atex2-0bOLDN  41137  4atex2-0cOLDN  41138  trlval4  41246  cdlemc5  41253  cdlemd5  41260  cdlemd6  41261  cdleme00a  41267  cdleme3g  41292  cdleme3h  41293  cdleme3  41295  cdleme4  41296  cdleme4a  41297  cdleme16aN  41317  cdleme11c  41319  cdleme11g  41323  cdleme11h  41324  cdleme12  41329  cdleme0nex  41348  cdleme18a  41349  cdleme18b  41350  cdleme18c  41351  cdleme18d  41353  cdleme20zN  41359  cdleme20y  41360  cdleme19a  41361  cdleme19b  41362  cdleme19d  41364  cdleme19e  41365  cdleme20aN  41367  cdleme20c  41369  cdleme20d  41370  cdleme20i  41375  cdleme20j  41376  cdleme20l1  41378  cdleme20l2  41379  cdleme20m  41381  cdleme21b  41384  cdleme21c  41385  cdleme21j  41394  cdleme22aa  41397  cdleme22a  41398  cdleme22eALTN  41403  cdleme26e  41417  cdleme26fALTN  41420  cdleme26f  41421  cdleme26f2ALTN  41422  cdleme26f2  41423  cdleme27N  41427  cdleme28a  41428  cdleme28b  41429  cdleme30a  41436  cdlemefs45eN  41489  cdleme32c  41501  cdleme32e  41503  cdleme35h  41514  cdleme36a  41518  cdleme36m  41519  cdleme37m  41520  cdleme41sn3aw  41532  cdleme41sn4aw  41533  cdleme41fva11  41535  cdleme42k  41542  cdleme43cN  41549  cdleme43dN  41550  cdleme46f2g1  41552  cdlemeg47rv2  41568  cdlemeg46sfg  41578  cdlemeg46fjgN  41579  cdlemeg46rjgN  41580  cdlemeg46fjv  41581  cdlemeg46frv  41583  cdlemeg46vrg  41585  cdlemeg46rgv  41586  cdlemeg46req  41587  cdlemeg46gfv  41588  cdleme50trn2a  41608  cdlemg2fv2  41658  cdlemg4a  41666  cdlemg4e  41672  cdlemg4f  41673  cdlemg8b  41686  cdlemg8c  41687  cdlemg9a  41690  cdlemg9b  41691  cdlemg9  41692  cdlemg10a  41698  cdlemg12a  41701  cdlemg12b  41702  cdlemg12c  41703  cdlemg12  41708  cdlemg17dN  41721  cdlemg17dALTN  41722  cdlemg17e  41723  cdlemg17i  41727  cdlemg17ir  41728  cdlemg17pq  41730  cdlemg17bq  41731  cdlemg17iqN  41732  cdlemg17  41735  cdlemg18b  41737  cdlemg18c  41738  cdlemg18d  41739  cdlemg18  41740  cdlemg19  41742  cdlemg21  41744  cdlemg28a  41751  cdlemg31b0a  41753  cdlemg33b0  41759  cdlemg35  41771  cdlemg44a  41789  cdlemh  41875  cdlemi2  41877  cdlemj1  41879  cdlemk5a  41893  cdlemk5  41894  cdlemki  41899  cdlemkvcl  41900  cdlemk10  41901  cdlemksv2  41905  cdlemk7  41906  cdlemk11  41907  cdlemk12  41908  cdlemk15  41913  cdlemk16a  41914  cdlemk16  41915  cdlemk5u  41919  cdlemk6u  41920  cdlemk18  41926  cdlemk19  41927  cdlemk7u  41928  cdlemk11u  41929  cdlemk12u  41930  cdlemk21N  41931  cdlemk20  41932  cdlemkoatnle-2N  41933  cdlemk13-2N  41934  cdlemkole-2N  41935  cdlemk14-2N  41936  cdlemk15-2N  41937  cdlemk16-2N  41938  cdlemk17-2N  41939  cdlemk18-2N  41944  cdlemk19-2N  41945  cdlemk22  41951  cdlemk30  41952  cdlemk28-3  41966  cdlemk33N  41967  cdlemkfid1N  41979  cdlemkid1  41980  cdlemky  41984  cdlemk11ta  41987  cdlemk35s-id  41996  cdlemk39s-id  41998  cdlemk47  42007  cdlemk48  42008  cdlemk49  42009  cdlemk50  42010  cdlemk51  42011  cdlemk52  42012  cdlemk53a  42013  cdlemk53b  42014  cdlemk53  42015  cdlemk54  42016  cdlemk55a  42017  cdlemkyyN  42020  cdlemk43N  42021  cdlemk55u1  42023  cdlemk55u  42024  cdlemk39u1  42025  cdlemk19u1  42027  cdleml1N  42034  cdleml2N  42035  cdleml3N  42036  dia2dimlem6  42127  cdlemn2  42253  cdlemn2a  42254  cdlemn5pre  42258  cdlemn11pre  42268  dihjustlem  42274  dihjust  42275  dihmeetlem15N  42379  lclkrlem2y  42589  relexpxpnnidm  44703  ormkglobd  47887  iscnrm3llem1  50057  iscnrm3l  50059  swapffunc  50390  fucofunc  50467