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  27488  f1otrg  28122  colinearalg  28168  ax5seglem6  28192  ax5seg  28196  axpasch  28199  axeuclid  28221  uhgr2edg  28465  clwwlkccat  29243  ogrpsub  32234  ogrpsublt  32239  rhmdvd  32436  bnj966  33955  bnj967  33956  mclspps  34575  cgrtr  34964  cgrtr3  34966  ofscom  34979  btwnxfr  35028  colinearxfr  35047  lineext  35048  brofs2  35049  brifs2  35050  fscgr  35052  linecgr  35053  btwnconn1lem1  35059  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem7  35065  seglecgr12im  35082  seglecgr12  35083  segletr  35086  broutsideof3  35098  outsideofeq  35102  lineunray  35119  eqlkr  37969  omlmod1i2N  38130  cvrcmp2  38154  cvlexch2  38199  cvlexchb2  38201  cvlatexchb2  38205  cvlatexch1  38206  cvlatexch2  38207  cvlatexch3  38208  cvlsupr7  38218  cvlsupr8  38219  atnlej1  38250  atnlej2  38251  2llnneN  38280  cvratlem  38292  atcvrneN  38301  atcvrj1  38302  atlelt  38309  2atjm  38316  3noncolr2  38320  3noncolr1N  38321  hlatcon2  38323  3dimlem2  38330  3dim1  38338  3dim2  38339  1cvrat  38347  ps-1  38348  ps-2  38349  2atjlej  38350  hlatexch3N  38351  ps-2b  38353  3atlem1  38354  3atlem2  38355  3atlem6  38359  llnle  38389  2atm  38398  ps-2c  38399  lplni2  38408  lplnle  38411  lplnnle2at  38412  lplnri3N  38426  llncvrlpln2  38428  2atmat  38432  2llnjaN  38437  2llnm2N  38439  2llnm4  38441  2llnmeqat  38442  lvolnle3at  38453  4atlem0ae  38465  4atlem0be  38466  4atlem3b  38469  4atlem9  38474  4atlem10a  38475  4atlem10  38477  4atlem11a  38478  4atlem12a  38481  4at  38484  4at2  38485  lplncvrlvol2  38486  2lplnm2N  38492  2llnma1b  38657  2llnma1  38658  2llnma3r  38659  2llnma2  38660  2llnma2rN  38661  cdlema1N  38662  cdlema2N  38663  paddasslem2  38692  paddasslem15  38705  paddasslem16  38706  pmodlem1  38717  pmod2iN  38720  hlmod1i  38727  atmod2i1  38732  atmod2i2  38733  atmod3i1  38735  atmod3i2  38736  atmod4i1  38737  atmod4i2  38738  llnexchb2  38740  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem13  38754  dalawlem15  38756  osumcllem7N  38833  osumcllem9N  38835  osumcllem11N  38837  pl42lem1N  38850  4atex  38947  4atex2-0aOLDN  38949  4atex2-0bOLDN  38950  4atex2-0cOLDN  38951  trlval4  39059  cdlemc5  39066  cdlemd5  39073  cdlemd6  39074  cdleme00a  39080  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme16aN  39130  cdleme11c  39132  cdleme11g  39136  cdleme11h  39137  cdleme12  39142  cdleme0nex  39161  cdleme18a  39162  cdleme18b  39163  cdleme18c  39164  cdleme18d  39166  cdleme20zN  39172  cdleme20y  39173  cdleme19a  39174  cdleme19b  39175  cdleme19d  39177  cdleme19e  39178  cdleme20aN  39180  cdleme20c  39182  cdleme20d  39183  cdleme20i  39188  cdleme20j  39189  cdleme20l1  39191  cdleme20l2  39192  cdleme20m  39194  cdleme21b  39197  cdleme21c  39198  cdleme21j  39207  cdleme22aa  39210  cdleme22a  39211  cdleme22eALTN  39216  cdleme26e  39230  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme27N  39240  cdleme28a  39241  cdleme28b  39242  cdleme30a  39249  cdlemefs45eN  39302  cdleme32c  39314  cdleme32e  39316  cdleme35h  39327  cdleme36a  39331  cdleme36m  39332  cdleme37m  39333  cdleme41sn3aw  39345  cdleme41sn4aw  39346  cdleme41fva11  39348  cdleme42k  39355  cdleme43cN  39362  cdleme43dN  39363  cdleme46f2g1  39365  cdlemeg47rv2  39381  cdlemeg46sfg  39391  cdlemeg46fjgN  39392  cdlemeg46rjgN  39393  cdlemeg46fjv  39394  cdlemeg46frv  39396  cdlemeg46vrg  39398  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemeg46gfv  39401  cdleme50trn2a  39421  cdlemg2fv2  39471  cdlemg4a  39479  cdlemg4e  39485  cdlemg4f  39486  cdlemg8b  39499  cdlemg8c  39500  cdlemg9a  39503  cdlemg9b  39504  cdlemg9  39505  cdlemg10a  39511  cdlemg12a  39514  cdlemg12b  39515  cdlemg12c  39516  cdlemg12  39521  cdlemg17dN  39534  cdlemg17dALTN  39535  cdlemg17e  39536  cdlemg17i  39540  cdlemg17ir  39541  cdlemg17pq  39543  cdlemg17bq  39544  cdlemg17iqN  39545  cdlemg17  39548  cdlemg18b  39550  cdlemg18c  39551  cdlemg18d  39552  cdlemg18  39553  cdlemg19  39555  cdlemg21  39557  cdlemg28a  39564  cdlemg31b0a  39566  cdlemg33b0  39572  cdlemg35  39584  cdlemg44a  39602  cdlemh  39688  cdlemi2  39690  cdlemj1  39692  cdlemk5a  39706  cdlemk5  39707  cdlemki  39712  cdlemkvcl  39713  cdlemk10  39714  cdlemksv2  39718  cdlemk7  39719  cdlemk11  39720  cdlemk12  39721  cdlemk15  39726  cdlemk16a  39727  cdlemk16  39728  cdlemk5u  39732  cdlemk6u  39733  cdlemk18  39739  cdlemk19  39740  cdlemk7u  39741  cdlemk11u  39742  cdlemk12u  39743  cdlemk21N  39744  cdlemk20  39745  cdlemkoatnle-2N  39746  cdlemk13-2N  39747  cdlemkole-2N  39748  cdlemk14-2N  39749  cdlemk15-2N  39750  cdlemk16-2N  39751  cdlemk17-2N  39752  cdlemk18-2N  39757  cdlemk19-2N  39758  cdlemk22  39764  cdlemk30  39765  cdlemk28-3  39779  cdlemk33N  39780  cdlemkfid1N  39792  cdlemkid1  39793  cdlemky  39797  cdlemk11ta  39800  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk47  39820  cdlemk48  39821  cdlemk49  39822  cdlemk50  39823  cdlemk51  39824  cdlemk52  39825  cdlemk53a  39826  cdlemk53b  39827  cdlemk53  39828  cdlemk54  39829  cdlemk55a  39830  cdlemkyyN  39833  cdlemk43N  39834  cdlemk55u1  39836  cdlemk55u  39837  cdlemk39u1  39838  cdlemk19u1  39840  cdleml1N  39847  cdleml2N  39848  cdleml3N  39849  dia2dimlem6  39940  cdlemn2  40066  cdlemn2a  40067  cdlemn5pre  40071  cdlemn11pre  40081  dihjustlem  40087  dihjust  40088  dihmeetlem15N  40192  lclkrlem2y  40402  relexpxpnnidm  42454  natglobalincr  45591  iscnrm3llem1  47582  iscnrm3l  47584