Theorem simp23 1210

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp123  1309  simp223  1318  simp323  1327  omeulem1  8519  elfiun  9345  ttrclselem2  9647  cofsmo  10191  modexp  14173  iscatd2  17616  funcoppc  17811  funcres  17832  catcisolem  18046  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  pmtrprfv3  19395  ogrpsub  20078  ogrpsublt  20083  mdetunilem3  22570  mdetunilem4  22571  mdetuni0  22577  mdetmul  22579  prdsxmetlem  24324  isosctrlem3  26798  isosctr  26799  noinfbnd2lem1  27710  addsass  28013  f1otrg  28955  colinearalg  28995  ax5seglem6  29019  ax5seg  29023  axpasch  29026  axeuclid  29048  uhgr2edg  29293  clwwlkccat  30077  rhmdvd  33416  bnj966  35119  bnj967  35120  mclspps  35797  cgrtr  36205  cgrtr3  36207  ofscom  36220  btwnxfr  36269  colinearxfr  36288  lineext  36289  brofs2  36290  brifs2  36291  fscgr  36293  linecgr  36294  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  seglecgr12im  36323  seglecgr12  36324  segletr  36327  broutsideof3  36339  outsideofeq  36343  lineunray  36360  eqlkr  39472  omlmod1i2N  39633  cvrcmp2  39657  cvlexch2  39702  cvlexchb2  39704  cvlatexchb2  39708  cvlatexch1  39709  cvlatexch2  39710  cvlatexch3  39711  cvlsupr7  39721  cvlsupr8  39722  atnlej1  39752  atnlej2  39753  2llnneN  39782  cvratlem  39794  atcvrneN  39803  atcvrj1  39804  atlelt  39811  2atjm  39818  3noncolr2  39822  3noncolr1N  39823  hlatcon2  39825  3dimlem2  39832  3dim1  39840  3dim2  39841  1cvrat  39849  ps-1  39850  ps-2  39851  2atjlej  39852  hlatexch3N  39853  ps-2b  39855  3atlem1  39856  3atlem2  39857  3atlem6  39861  llnle  39891  2atm  39900  ps-2c  39901  lplni2  39910  lplnle  39913  lplnnle2at  39914  lplnri3N  39928  llncvrlpln2  39930  2atmat  39934  2llnjaN  39939  2llnm2N  39941  2llnm4  39943  2llnmeqat  39944  lvolnle3at  39955  4atlem0ae  39967  4atlem0be  39968  4atlem3b  39971  4atlem9  39976  4atlem10a  39977  4atlem10  39979  4atlem11a  39980  4atlem12a  39983  4at  39986  4at2  39987  lplncvrlvol2  39988  2lplnm2N  39994  2llnma1b  40159  2llnma1  40160  2llnma3r  40161  2llnma2  40162  2llnma2rN  40163  cdlema1N  40164  cdlema2N  40165  paddasslem2  40194  paddasslem15  40207  paddasslem16  40208  pmodlem1  40219  pmod2iN  40222  hlmod1i  40229  atmod2i1  40234  atmod2i2  40235  atmod3i1  40237  atmod3i2  40238  atmod4i1  40239  atmod4i2  40240  llnexchb2  40242  dalawlem3  40246  dalawlem4  40247  dalawlem5  40248  dalawlem6  40249  dalawlem7  40250  dalawlem8  40251  dalawlem9  40252  dalawlem11  40254  dalawlem13  40256  dalawlem15  40258  osumcllem7N  40335  osumcllem9N  40337  osumcllem11N  40339  pl42lem1N  40352  4atex  40449  4atex2-0aOLDN  40451  4atex2-0bOLDN  40452  4atex2-0cOLDN  40453  trlval4  40561  cdlemc5  40568  cdlemd5  40575  cdlemd6  40576  cdleme00a  40582  cdleme3g  40607  cdleme3h  40608  cdleme3  40610  cdleme4  40611  cdleme4a  40612  cdleme16aN  40632  cdleme11c  40634  cdleme11g  40638  cdleme11h  40639  cdleme12  40644  cdleme0nex  40663  cdleme18a  40664  cdleme18b  40665  cdleme18c  40666  cdleme18d  40668  cdleme20zN  40674  cdleme20y  40675  cdleme19a  40676  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20aN  40682  cdleme20c  40684  cdleme20d  40685  cdleme20i  40690  cdleme20j  40691  cdleme20l1  40693  cdleme20l2  40694  cdleme20m  40696  cdleme21b  40699  cdleme21c  40700  cdleme21j  40709  cdleme22aa  40712  cdleme22a  40713  cdleme22eALTN  40718  cdleme26e  40732  cdleme26fALTN  40735  cdleme26f  40736  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme27N  40742  cdleme28a  40743  cdleme28b  40744  cdleme30a  40751  cdlemefs45eN  40804  cdleme32c  40816  cdleme32e  40818  cdleme35h  40829  cdleme36a  40833  cdleme36m  40834  cdleme37m  40835  cdleme41sn3aw  40847  cdleme41sn4aw  40848  cdleme41fva11  40850  cdleme42k  40857  cdleme43cN  40864  cdleme43dN  40865  cdleme46f2g1  40867  cdlemeg47rv2  40883  cdlemeg46sfg  40893  cdlemeg46fjgN  40894  cdlemeg46rjgN  40895  cdlemeg46fjv  40896  cdlemeg46frv  40898  cdlemeg46vrg  40900  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemeg46gfv  40903  cdleme50trn2a  40923  cdlemg2fv2  40973  cdlemg4a  40981  cdlemg4e  40987  cdlemg4f  40988  cdlemg8b  41001  cdlemg8c  41002  cdlemg9a  41005  cdlemg9b  41006  cdlemg9  41007  cdlemg10a  41013  cdlemg12a  41016  cdlemg12b  41017  cdlemg12c  41018  cdlemg12  41023  cdlemg17dN  41036  cdlemg17dALTN  41037  cdlemg17e  41038  cdlemg17i  41042  cdlemg17ir  41043  cdlemg17pq  41045  cdlemg17bq  41046  cdlemg17iqN  41047  cdlemg17  41050  cdlemg18b  41052  cdlemg18c  41053  cdlemg18d  41054  cdlemg18  41055  cdlemg19  41057  cdlemg21  41059  cdlemg28a  41066  cdlemg31b0a  41068  cdlemg33b0  41074  cdlemg35  41086  cdlemg44a  41104  cdlemh  41190  cdlemi2  41192  cdlemj1  41194  cdlemk5a  41208  cdlemk5  41209  cdlemki  41214  cdlemkvcl  41215  cdlemk10  41216  cdlemksv2  41220  cdlemk7  41221  cdlemk11  41222  cdlemk12  41223  cdlemk15  41228  cdlemk16a  41229  cdlemk16  41230  cdlemk5u  41234  cdlemk6u  41235  cdlemk18  41241  cdlemk19  41242  cdlemk7u  41243  cdlemk11u  41244  cdlemk12u  41245  cdlemk21N  41246  cdlemk20  41247  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk22  41266  cdlemk30  41267  cdlemk28-3  41281  cdlemk33N  41282  cdlemkfid1N  41294  cdlemkid1  41295  cdlemky  41299  cdlemk11ta  41302  cdlemk35s-id  41311  cdlemk39s-id  41313  cdlemk47  41322  cdlemk48  41323  cdlemk49  41324  cdlemk50  41325  cdlemk51  41326  cdlemk52  41327  cdlemk53a  41328  cdlemk53b  41329  cdlemk53  41330  cdlemk54  41331  cdlemk55a  41332  cdlemkyyN  41335  cdlemk43N  41336  cdlemk55u1  41338  cdlemk55u  41339  cdlemk39u1  41340  cdlemk19u1  41342  cdleml1N  41349  cdleml2N  41350  cdleml3N  41351  dia2dimlem6  41442  cdlemn2  41568  cdlemn2a  41569  cdlemn5pre  41573  cdlemn11pre  41583  dihjustlem  41589  dihjust  41590  dihmeetlem15N  41694  lclkrlem2y  41904  relexpxpnnidm  44056  ormkglobd  47230  natglobalincr  47232  iscnrm3llem1  49305  iscnrm3l  49307  swapffunc  49638  fucofunc  49715