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 210  df-an 400  df-3an 1090

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8232  elfiun  8960  cofsmo  9762  modexp  13684  iscatd2  17048  funcoppc  17243  funcres  17264  catcisolem  17475  1stfcl  17556  2ndfcl  17557  prfcl  17562  evlfcl  17581  curf1cl  17587  curfcl  17591  hofcl  17618  pmtrprfv3  18693  mdetunilem3  21358  mdetunilem4  21359  mdetuni0  21365  mdetmul  21367  prdsxmetlem  23114  isosctrlem3  25550  isosctr  25551  f1otrg  26809  colinearalg  26848  ax5seglem6  26872  ax5seg  26876  axpasch  26879  axeuclid  26901  uhgr2edg  27142  clwwlkccat  27919  ogrpsub  30911  ogrpsublt  30916  rhmdvd  31089  bnj966  32487  bnj967  32488  mclspps  33109  noinfbnd2lem1  33566  cgrtr  33924  cgrtr3  33926  ofscom  33939  btwnxfr  33988  colinearxfr  34007  lineext  34008  brofs2  34009  brifs2  34010  fscgr  34012  linecgr  34013  btwnconn1lem1  34019  btwnconn1lem2  34020  btwnconn1lem3  34021  btwnconn1lem4  34022  btwnconn1lem5  34023  btwnconn1lem6  34024  btwnconn1lem7  34025  seglecgr12im  34042  seglecgr12  34043  segletr  34046  broutsideof3  34058  outsideofeq  34062  lineunray  34079  eqlkr  36725  omlmod1i2N  36886  cvrcmp2  36910  cvlexch2  36955  cvlexchb2  36957  cvlatexchb2  36961  cvlatexch1  36962  cvlatexch2  36963  cvlatexch3  36964  cvlsupr7  36974  cvlsupr8  36975  atnlej1  37005  atnlej2  37006  2llnneN  37035  cvratlem  37047  atcvrneN  37056  atcvrj1  37057  atlelt  37064  2atjm  37071  3noncolr2  37075  3noncolr1N  37076  hlatcon2  37078  3dimlem2  37085  3dim1  37093  3dim2  37094  1cvrat  37102  ps-1  37103  ps-2  37104  2atjlej  37105  hlatexch3N  37106  ps-2b  37108  3atlem1  37109  3atlem2  37110  3atlem6  37114  llnle  37144  2atm  37153  ps-2c  37154  lplni2  37163  lplnle  37166  lplnnle2at  37167  lplnri3N  37181  llncvrlpln2  37183  2atmat  37187  2llnjaN  37192  2llnm2N  37194  2llnm4  37196  2llnmeqat  37197  lvolnle3at  37208  4atlem0ae  37220  4atlem0be  37221  4atlem3b  37224  4atlem9  37229  4atlem10a  37230  4atlem10  37232  4atlem11a  37233  4atlem12a  37236  4at  37239  4at2  37240  lplncvrlvol2  37241  2lplnm2N  37247  2llnma1b  37412  2llnma1  37413  2llnma3r  37414  2llnma2  37415  2llnma2rN  37416  cdlema1N  37417  cdlema2N  37418  paddasslem2  37447  paddasslem15  37460  paddasslem16  37461  pmodlem1  37472  pmod2iN  37475  hlmod1i  37482  atmod2i1  37487  atmod2i2  37488  atmod3i1  37490  atmod3i2  37491  atmod4i1  37492  atmod4i2  37493  llnexchb2  37495  dalawlem3  37499  dalawlem4  37500  dalawlem5  37501  dalawlem6  37502  dalawlem7  37503  dalawlem8  37504  dalawlem9  37505  dalawlem11  37507  dalawlem13  37509  dalawlem15  37511  osumcllem7N  37588  osumcllem9N  37590  osumcllem11N  37592  pl42lem1N  37605  4atex  37702  4atex2-0aOLDN  37704  4atex2-0bOLDN  37705  4atex2-0cOLDN  37706  trlval4  37814  cdlemc5  37821  cdlemd5  37828  cdlemd6  37829  cdleme00a  37835  cdleme3g  37860  cdleme3h  37861  cdleme3  37863  cdleme4  37864  cdleme4a  37865  cdleme16aN  37885  cdleme11c  37887  cdleme11g  37891  cdleme11h  37892  cdleme12  37897  cdleme0nex  37916  cdleme18a  37917  cdleme18b  37918  cdleme18c  37919  cdleme18d  37921  cdleme20zN  37927  cdleme20y  37928  cdleme19a  37929  cdleme19b  37930  cdleme19d  37932  cdleme19e  37933  cdleme20aN  37935  cdleme20c  37937  cdleme20d  37938  cdleme20i  37943  cdleme20j  37944  cdleme20l1  37946  cdleme20l2  37947  cdleme20m  37949  cdleme21b  37952  cdleme21c  37953  cdleme21j  37962  cdleme22aa  37965  cdleme22a  37966  cdleme22eALTN  37971  cdleme26e  37985  cdleme26fALTN  37988  cdleme26f  37989  cdleme26f2ALTN  37990  cdleme26f2  37991  cdleme27N  37995  cdleme28a  37996  cdleme28b  37997  cdleme30a  38004  cdlemefs45eN  38057  cdleme32c  38069  cdleme32e  38071  cdleme35h  38082  cdleme36a  38086  cdleme36m  38087  cdleme37m  38088  cdleme41sn3aw  38100  cdleme41sn4aw  38101  cdleme41fva11  38103  cdleme42k  38110  cdleme43cN  38117  cdleme43dN  38118  cdleme46f2g1  38120  cdlemeg47rv2  38136  cdlemeg46sfg  38146  cdlemeg46fjgN  38147  cdlemeg46rjgN  38148  cdlemeg46fjv  38149  cdlemeg46frv  38151  cdlemeg46vrg  38153  cdlemeg46rgv  38154  cdlemeg46req  38155  cdlemeg46gfv  38156  cdleme50trn2a  38176  cdlemg2fv2  38226  cdlemg4a  38234  cdlemg4e  38240  cdlemg4f  38241  cdlemg8b  38254  cdlemg8c  38255  cdlemg9a  38258  cdlemg9b  38259  cdlemg9  38260  cdlemg10a  38266  cdlemg12a  38269  cdlemg12b  38270  cdlemg12c  38271  cdlemg12  38276  cdlemg17dN  38289  cdlemg17dALTN  38290  cdlemg17e  38291  cdlemg17i  38295  cdlemg17ir  38296  cdlemg17pq  38298  cdlemg17bq  38299  cdlemg17iqN  38300  cdlemg17  38303  cdlemg18b  38305  cdlemg18c  38306  cdlemg18d  38307  cdlemg18  38308  cdlemg19  38310  cdlemg21  38312  cdlemg28a  38319  cdlemg31b0a  38321  cdlemg33b0  38327  cdlemg35  38339  cdlemg44a  38357  cdlemh  38443  cdlemi2  38445  cdlemj1  38447  cdlemk5a  38461  cdlemk5  38462  cdlemki  38467  cdlemkvcl  38468  cdlemk10  38469  cdlemksv2  38473  cdlemk7  38474  cdlemk11  38475  cdlemk12  38476  cdlemk15  38481  cdlemk16a  38482  cdlemk16  38483  cdlemk5u  38487  cdlemk6u  38488  cdlemk18  38494  cdlemk19  38495  cdlemk7u  38496  cdlemk11u  38497  cdlemk12u  38498  cdlemk21N  38499  cdlemk20  38500  cdlemkoatnle-2N  38501  cdlemk13-2N  38502  cdlemkole-2N  38503  cdlemk14-2N  38504  cdlemk15-2N  38505  cdlemk16-2N  38506  cdlemk17-2N  38507  cdlemk18-2N  38512  cdlemk19-2N  38513  cdlemk22  38519  cdlemk30  38520  cdlemk28-3  38534  cdlemk33N  38535  cdlemkfid1N  38547  cdlemkid1  38548  cdlemky  38552  cdlemk11ta  38555  cdlemk35s-id  38564  cdlemk39s-id  38566  cdlemk47  38575  cdlemk48  38576  cdlemk49  38577  cdlemk50  38578  cdlemk51  38579  cdlemk52  38580  cdlemk53a  38581  cdlemk53b  38582  cdlemk53  38583  cdlemk54  38584  cdlemk55a  38585  cdlemkyyN  38588  cdlemk43N  38589  cdlemk55u1  38591  cdlemk55u  38592  cdlemk39u1  38593  cdlemk19u1  38595  cdleml1N  38602  cdleml2N  38603  cdleml3N  38604  dia2dimlem6  38695  cdlemn2  38821  cdlemn2a  38822  cdlemn5pre  38826  cdlemn11pre  38836  dihjustlem  38842  dihjust  38843  dihmeetlem15N  38947  lclkrlem2y  39157  relexpxpnnidm  40841  iscnrm3llem1  45749  iscnrm3l  45751