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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8582  elfiun  9425  ttrclselem2  9721  cofsmo  10264  modexp  14201  iscatd2  17625  funcoppc  17825  funcres  17846  catcisolem  18060  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  pmtrprfv3  19322  mdetunilem3  22116  mdetunilem4  22117  mdetuni0  22123  mdetmul  22125  prdsxmetlem  23874  isosctrlem3  26325  isosctr  26326  noinfbnd2lem1  27233  addsass  27491  f1otrg  28153  colinearalg  28199  ax5seglem6  28223  ax5seg  28227  axpasch  28230  axeuclid  28252  uhgr2edg  28496  clwwlkccat  29274  ogrpsub  32265  ogrpsublt  32270  rhmdvd  32467  bnj966  33986  bnj967  33987  mclspps  34606  cgrtr  34995  cgrtr3  34997  ofscom  35010  btwnxfr  35059  colinearxfr  35078  lineext  35079  brofs2  35080  brifs2  35081  fscgr  35083  linecgr  35084  btwnconn1lem1  35090  btwnconn1lem2  35091  btwnconn1lem3  35092  btwnconn1lem4  35093  btwnconn1lem5  35094  btwnconn1lem6  35095  btwnconn1lem7  35096  seglecgr12im  35113  seglecgr12  35114  segletr  35117  broutsideof3  35129  outsideofeq  35133  lineunray  35150  eqlkr  38017  omlmod1i2N  38178  cvrcmp2  38202  cvlexch2  38247  cvlexchb2  38249  cvlatexchb2  38253  cvlatexch1  38254  cvlatexch2  38255  cvlatexch3  38256  cvlsupr7  38266  cvlsupr8  38267  atnlej1  38298  atnlej2  38299  2llnneN  38328  cvratlem  38340  atcvrneN  38349  atcvrj1  38350  atlelt  38357  2atjm  38364  3noncolr2  38368  3noncolr1N  38369  hlatcon2  38371  3dimlem2  38378  3dim1  38386  3dim2  38387  1cvrat  38395  ps-1  38396  ps-2  38397  2atjlej  38398  hlatexch3N  38399  ps-2b  38401  3atlem1  38402  3atlem2  38403  3atlem6  38407  llnle  38437  2atm  38446  ps-2c  38447  lplni2  38456  lplnle  38459  lplnnle2at  38460  lplnri3N  38474  llncvrlpln2  38476  2atmat  38480  2llnjaN  38485  2llnm2N  38487  2llnm4  38489  2llnmeqat  38490  lvolnle3at  38501  4atlem0ae  38513  4atlem0be  38514  4atlem3b  38517  4atlem9  38522  4atlem10a  38523  4atlem10  38525  4atlem11a  38526  4atlem12a  38529  4at  38532  4at2  38533  lplncvrlvol2  38534  2lplnm2N  38540  2llnma1b  38705  2llnma1  38706  2llnma3r  38707  2llnma2  38708  2llnma2rN  38709  cdlema1N  38710  cdlema2N  38711  paddasslem2  38740  paddasslem15  38753  paddasslem16  38754  pmodlem1  38765  pmod2iN  38768  hlmod1i  38775  atmod2i1  38780  atmod2i2  38781  atmod3i1  38783  atmod3i2  38784  atmod4i1  38785  atmod4i2  38786  llnexchb2  38788  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem13  38802  dalawlem15  38804  osumcllem7N  38881  osumcllem9N  38883  osumcllem11N  38885  pl42lem1N  38898  4atex  38995  4atex2-0aOLDN  38997  4atex2-0bOLDN  38998  4atex2-0cOLDN  38999  trlval4  39107  cdlemc5  39114  cdlemd5  39121  cdlemd6  39122  cdleme00a  39128  cdleme3g  39153  cdleme3h  39154  cdleme3  39156  cdleme4  39157  cdleme4a  39158  cdleme16aN  39178  cdleme11c  39180  cdleme11g  39184  cdleme11h  39185  cdleme12  39190  cdleme0nex  39209  cdleme18a  39210  cdleme18b  39211  cdleme18c  39212  cdleme18d  39214  cdleme20zN  39220  cdleme20y  39221  cdleme19a  39222  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20aN  39228  cdleme20c  39230  cdleme20d  39231  cdleme20i  39236  cdleme20j  39237  cdleme20l1  39239  cdleme20l2  39240  cdleme20m  39242  cdleme21b  39245  cdleme21c  39246  cdleme21j  39255  cdleme22aa  39258  cdleme22a  39259  cdleme22eALTN  39264  cdleme26e  39278  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme27N  39288  cdleme28a  39289  cdleme28b  39290  cdleme30a  39297  cdlemefs45eN  39350  cdleme32c  39362  cdleme32e  39364  cdleme35h  39375  cdleme36a  39379  cdleme36m  39380  cdleme37m  39381  cdleme41sn3aw  39393  cdleme41sn4aw  39394  cdleme41fva11  39396  cdleme42k  39403  cdleme43cN  39410  cdleme43dN  39411  cdleme46f2g1  39413  cdlemeg47rv2  39429  cdlemeg46sfg  39439  cdlemeg46fjgN  39440  cdlemeg46rjgN  39441  cdlemeg46fjv  39442  cdlemeg46frv  39444  cdlemeg46vrg  39446  cdlemeg46rgv  39447  cdlemeg46req  39448  cdlemeg46gfv  39449  cdleme50trn2a  39469  cdlemg2fv2  39519  cdlemg4a  39527  cdlemg4e  39533  cdlemg4f  39534  cdlemg8b  39547  cdlemg8c  39548  cdlemg9a  39551  cdlemg9b  39552  cdlemg9  39553  cdlemg10a  39559  cdlemg12a  39562  cdlemg12b  39563  cdlemg12c  39564  cdlemg12  39569  cdlemg17dN  39582  cdlemg17dALTN  39583  cdlemg17e  39584  cdlemg17i  39588  cdlemg17ir  39589  cdlemg17pq  39591  cdlemg17bq  39592  cdlemg17iqN  39593  cdlemg17  39596  cdlemg18b  39598  cdlemg18c  39599  cdlemg18d  39600  cdlemg18  39601  cdlemg19  39603  cdlemg21  39605  cdlemg28a  39612  cdlemg31b0a  39614  cdlemg33b0  39620  cdlemg35  39632  cdlemg44a  39650  cdlemh  39736  cdlemi2  39738  cdlemj1  39740  cdlemk5a  39754  cdlemk5  39755  cdlemki  39760  cdlemkvcl  39761  cdlemk10  39762  cdlemksv2  39766  cdlemk7  39767  cdlemk11  39768  cdlemk12  39769  cdlemk15  39774  cdlemk16a  39775  cdlemk16  39776  cdlemk5u  39780  cdlemk6u  39781  cdlemk18  39787  cdlemk19  39788  cdlemk7u  39789  cdlemk11u  39790  cdlemk12u  39791  cdlemk21N  39792  cdlemk20  39793  cdlemkoatnle-2N  39794  cdlemk13-2N  39795  cdlemkole-2N  39796  cdlemk14-2N  39797  cdlemk15-2N  39798  cdlemk16-2N  39799  cdlemk17-2N  39800  cdlemk18-2N  39805  cdlemk19-2N  39806  cdlemk22  39812  cdlemk30  39813  cdlemk28-3  39827  cdlemk33N  39828  cdlemkfid1N  39840  cdlemkid1  39841  cdlemky  39845  cdlemk11ta  39848  cdlemk35s-id  39857  cdlemk39s-id  39859  cdlemk47  39868  cdlemk48  39869  cdlemk49  39870  cdlemk50  39871  cdlemk51  39872  cdlemk52  39873  cdlemk53a  39874  cdlemk53b  39875  cdlemk53  39876  cdlemk54  39877  cdlemk55a  39878  cdlemkyyN  39881  cdlemk43N  39882  cdlemk55u1  39884  cdlemk55u  39885  cdlemk39u1  39886  cdlemk19u1  39888  cdleml1N  39895  cdleml2N  39896  cdleml3N  39897  dia2dimlem6  39988  cdlemn2  40114  cdlemn2a  40115  cdlemn5pre  40119  cdlemn11pre  40129  dihjustlem  40135  dihjust  40136  dihmeetlem15N  40240  lclkrlem2y  40450  relexpxpnnidm  42502  natglobalincr  45639  iscnrm3llem1  47630  iscnrm3l  47632