Theorem simp23 1204

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp123  1303  simp223  1312  simp323  1321  omeulem1  8210  elfiun  8896  cofsmo  9693  modexp  13602  iscatd2  16954  funcoppc  17147  funcres  17168  catcisolem  17368  1stfcl  17449  2ndfcl  17450  prfcl  17455  evlfcl  17474  curf1cl  17480  curfcl  17484  hofcl  17511  pmtrprfv3  18584  mdetunilem3  21225  mdetunilem4  21226  mdetuni0  21232  mdetmul  21234  prdsxmetlem  22980  isosctrlem3  25400  isosctr  25401  f1otrg  26659  colinearalg  26698  ax5seglem6  26722  ax5seg  26726  axpasch  26729  axeuclid  26751  uhgr2edg  26992  clwwlkccat  27770  ogrpsub  30719  ogrpsublt  30724  rhmdvd  30896  bnj966  32218  bnj967  32219  mclspps  32833  cgrtr  33455  cgrtr3  33457  ofscom  33470  btwnxfr  33519  colinearxfr  33538  lineext  33539  brofs2  33540  brifs2  33541  fscgr  33543  linecgr  33544  btwnconn1lem1  33550  btwnconn1lem2  33551  btwnconn1lem3  33552  btwnconn1lem4  33553  btwnconn1lem5  33554  btwnconn1lem6  33555  btwnconn1lem7  33556  seglecgr12im  33573  seglecgr12  33574  segletr  33577  broutsideof3  33589  outsideofeq  33593  lineunray  33610  eqlkr  36237  omlmod1i2N  36398  cvrcmp2  36422  cvlexch2  36467  cvlexchb2  36469  cvlatexchb2  36473  cvlatexch1  36474  cvlatexch2  36475  cvlatexch3  36476  cvlsupr7  36486  cvlsupr8  36487  atnlej1  36517  atnlej2  36518  2llnneN  36547  cvratlem  36559  atcvrneN  36568  atcvrj1  36569  atlelt  36576  2atjm  36583  3noncolr2  36587  3noncolr1N  36588  hlatcon2  36590  3dimlem2  36597  3dim1  36605  3dim2  36606  1cvrat  36614  ps-1  36615  ps-2  36616  2atjlej  36617  hlatexch3N  36618  ps-2b  36620  3atlem1  36621  3atlem2  36622  3atlem6  36626  llnle  36656  2atm  36665  ps-2c  36666  lplni2  36675  lplnle  36678  lplnnle2at  36679  lplnri3N  36693  llncvrlpln2  36695  2atmat  36699  2llnjaN  36704  2llnm2N  36706  2llnm4  36708  2llnmeqat  36709  lvolnle3at  36720  4atlem0ae  36732  4atlem0be  36733  4atlem3b  36736  4atlem9  36741  4atlem10a  36742  4atlem10  36744  4atlem11a  36745  4atlem12a  36748  4at  36751  4at2  36752  lplncvrlvol2  36753  2lplnm2N  36759  2llnma1b  36924  2llnma1  36925  2llnma3r  36926  2llnma2  36927  2llnma2rN  36928  cdlema1N  36929  cdlema2N  36930  paddasslem2  36959  paddasslem15  36972  paddasslem16  36973  pmodlem1  36984  pmod2iN  36987  hlmod1i  36994  atmod2i1  36999  atmod2i2  37000  atmod3i1  37002  atmod3i2  37003  atmod4i1  37004  atmod4i2  37005  llnexchb2  37007  dalawlem3  37011  dalawlem4  37012  dalawlem5  37013  dalawlem6  37014  dalawlem7  37015  dalawlem8  37016  dalawlem9  37017  dalawlem11  37019  dalawlem13  37021  dalawlem15  37023  osumcllem7N  37100  osumcllem9N  37102  osumcllem11N  37104  pl42lem1N  37117  4atex  37214  4atex2-0aOLDN  37216  4atex2-0bOLDN  37217  4atex2-0cOLDN  37218  trlval4  37326  cdlemc5  37333  cdlemd5  37340  cdlemd6  37341  cdleme00a  37347  cdleme3g  37372  cdleme3h  37373  cdleme3  37375  cdleme4  37376  cdleme4a  37377  cdleme16aN  37397  cdleme11c  37399  cdleme11g  37403  cdleme11h  37404  cdleme12  37409  cdleme0nex  37428  cdleme18a  37429  cdleme18b  37430  cdleme18c  37431  cdleme18d  37433  cdleme20zN  37439  cdleme20y  37440  cdleme19a  37441  cdleme19b  37442  cdleme19d  37444  cdleme19e  37445  cdleme20aN  37447  cdleme20c  37449  cdleme20d  37450  cdleme20i  37455  cdleme20j  37456  cdleme20l1  37458  cdleme20l2  37459  cdleme20m  37461  cdleme21b  37464  cdleme21c  37465  cdleme21j  37474  cdleme22aa  37477  cdleme22a  37478  cdleme22eALTN  37483  cdleme26e  37497  cdleme26fALTN  37500  cdleme26f  37501  cdleme26f2ALTN  37502  cdleme26f2  37503  cdleme27N  37507  cdleme28a  37508  cdleme28b  37509  cdleme30a  37516  cdlemefs45eN  37569  cdleme32c  37581  cdleme32e  37583  cdleme35h  37594  cdleme36a  37598  cdleme36m  37599  cdleme37m  37600  cdleme41sn3aw  37612  cdleme41sn4aw  37613  cdleme41fva11  37615  cdleme42k  37622  cdleme43cN  37629  cdleme43dN  37630  cdleme46f2g1  37632  cdlemeg47rv2  37648  cdlemeg46sfg  37658  cdlemeg46fjgN  37659  cdlemeg46rjgN  37660  cdlemeg46fjv  37661  cdlemeg46frv  37663  cdlemeg46vrg  37665  cdlemeg46rgv  37666  cdlemeg46req  37667  cdlemeg46gfv  37668  cdleme50trn2a  37688  cdlemg2fv2  37738  cdlemg4a  37746  cdlemg4e  37752  cdlemg4f  37753  cdlemg8b  37766  cdlemg8c  37767  cdlemg9a  37770  cdlemg9b  37771  cdlemg9  37772  cdlemg10a  37778  cdlemg12a  37781  cdlemg12b  37782  cdlemg12c  37783  cdlemg12  37788  cdlemg17dN  37801  cdlemg17dALTN  37802  cdlemg17e  37803  cdlemg17i  37807  cdlemg17ir  37808  cdlemg17pq  37810  cdlemg17bq  37811  cdlemg17iqN  37812  cdlemg17  37815  cdlemg18b  37817  cdlemg18c  37818  cdlemg18d  37819  cdlemg18  37820  cdlemg19  37822  cdlemg21  37824  cdlemg28a  37831  cdlemg31b0a  37833  cdlemg33b0  37839  cdlemg35  37851  cdlemg44a  37869  cdlemh  37955  cdlemi2  37957  cdlemj1  37959  cdlemk5a  37973  cdlemk5  37974  cdlemki  37979  cdlemkvcl  37980  cdlemk10  37981  cdlemksv2  37985  cdlemk7  37986  cdlemk11  37987  cdlemk12  37988  cdlemk15  37993  cdlemk16a  37994  cdlemk16  37995  cdlemk5u  37999  cdlemk6u  38000  cdlemk18  38006  cdlemk19  38007  cdlemk7u  38008  cdlemk11u  38009  cdlemk12u  38010  cdlemk21N  38011  cdlemk20  38012  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk22  38031  cdlemk30  38032  cdlemk28-3  38046  cdlemk33N  38047  cdlemkfid1N  38059  cdlemkid1  38060  cdlemky  38064  cdlemk11ta  38067  cdlemk35s-id  38076  cdlemk39s-id  38078  cdlemk47  38087  cdlemk48  38088  cdlemk49  38089  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  cdlemk53a  38093  cdlemk53b  38094  cdlemk53  38095  cdlemk54  38096  cdlemk55a  38097  cdlemkyyN  38100  cdlemk43N  38101  cdlemk55u1  38103  cdlemk55u  38104  cdlemk39u1  38105  cdlemk19u1  38107  cdleml1N  38114  cdleml2N  38115  cdleml3N  38116  dia2dimlem6  38207  cdlemn2  38333  cdlemn2a  38334  cdlemn5pre  38338  cdlemn11pre  38348  dihjustlem  38354  dihjust  38355  dihmeetlem15N  38459  lclkrlem2y  38669  relexpxpnnidm  40055