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  8207  elfiun  8893  cofsmo  9690  modexp  13598  iscatd2  16951  funcoppc  17144  funcres  17165  catcisolem  17365  1stfcl  17446  2ndfcl  17447  prfcl  17452  evlfcl  17471  curf1cl  17477  curfcl  17481  hofcl  17508  pmtrprfv3  18581  mdetunilem3  21222  mdetunilem4  21223  mdetuni0  21229  mdetmul  21231  prdsxmetlem  22977  isosctrlem3  25397  isosctr  25398  f1otrg  26656  colinearalg  26695  ax5seglem6  26719  ax5seg  26723  axpasch  26726  axeuclid  26748  uhgr2edg  26989  clwwlkccat  27767  ogrpsub  30717  ogrpsublt  30722  rhmdvd  30894  bnj966  32216  bnj967  32217  mclspps  32831  cgrtr  33453  cgrtr3  33455  ofscom  33468  btwnxfr  33517  colinearxfr  33536  lineext  33537  brofs2  33538  brifs2  33539  fscgr  33541  linecgr  33542  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem7  33554  seglecgr12im  33571  seglecgr12  33572  segletr  33575  broutsideof3  33587  outsideofeq  33591  lineunray  33608  eqlkr  36234  omlmod1i2N  36395  cvrcmp2  36419  cvlexch2  36464  cvlexchb2  36466  cvlatexchb2  36470  cvlatexch1  36471  cvlatexch2  36472  cvlatexch3  36473  cvlsupr7  36483  cvlsupr8  36484  atnlej1  36514  atnlej2  36515  2llnneN  36544  cvratlem  36556  atcvrneN  36565  atcvrj1  36566  atlelt  36573  2atjm  36580  3noncolr2  36584  3noncolr1N  36585  hlatcon2  36587  3dimlem2  36594  3dim1  36602  3dim2  36603  1cvrat  36611  ps-1  36612  ps-2  36613  2atjlej  36614  hlatexch3N  36615  ps-2b  36617  3atlem1  36618  3atlem2  36619  3atlem6  36623  llnle  36653  2atm  36662  ps-2c  36663  lplni2  36672  lplnle  36675  lplnnle2at  36676  lplnri3N  36690  llncvrlpln2  36692  2atmat  36696  2llnjaN  36701  2llnm2N  36703  2llnm4  36705  2llnmeqat  36706  lvolnle3at  36717  4atlem0ae  36729  4atlem0be  36730  4atlem3b  36733  4atlem9  36738  4atlem10a  36739  4atlem10  36741  4atlem11a  36742  4atlem12a  36745  4at  36748  4at2  36749  lplncvrlvol2  36750  2lplnm2N  36756  2llnma1b  36921  2llnma1  36922  2llnma3r  36923  2llnma2  36924  2llnma2rN  36925  cdlema1N  36926  cdlema2N  36927  paddasslem2  36956  paddasslem15  36969  paddasslem16  36970  pmodlem1  36981  pmod2iN  36984  hlmod1i  36991  atmod2i1  36996  atmod2i2  36997  atmod3i1  36999  atmod3i2  37000  atmod4i1  37001  atmod4i2  37002  llnexchb2  37004  dalawlem3  37008  dalawlem4  37009  dalawlem5  37010  dalawlem6  37011  dalawlem7  37012  dalawlem8  37013  dalawlem9  37014  dalawlem11  37016  dalawlem13  37018  dalawlem15  37020  osumcllem7N  37097  osumcllem9N  37099  osumcllem11N  37101  pl42lem1N  37114  4atex  37211  4atex2-0aOLDN  37213  4atex2-0bOLDN  37214  4atex2-0cOLDN  37215  trlval4  37323  cdlemc5  37330  cdlemd5  37337  cdlemd6  37338  cdleme00a  37344  cdleme3g  37369  cdleme3h  37370  cdleme3  37372  cdleme4  37373  cdleme4a  37374  cdleme16aN  37394  cdleme11c  37396  cdleme11g  37400  cdleme11h  37401  cdleme12  37406  cdleme0nex  37425  cdleme18a  37426  cdleme18b  37427  cdleme18c  37428  cdleme18d  37430  cdleme20zN  37436  cdleme20y  37437  cdleme19a  37438  cdleme19b  37439  cdleme19d  37441  cdleme19e  37442  cdleme20aN  37444  cdleme20c  37446  cdleme20d  37447  cdleme20i  37452  cdleme20j  37453  cdleme20l1  37455  cdleme20l2  37456  cdleme20m  37458  cdleme21b  37461  cdleme21c  37462  cdleme21j  37471  cdleme22aa  37474  cdleme22a  37475  cdleme22eALTN  37480  cdleme26e  37494  cdleme26fALTN  37497  cdleme26f  37498  cdleme26f2ALTN  37499  cdleme26f2  37500  cdleme27N  37504  cdleme28a  37505  cdleme28b  37506  cdleme30a  37513  cdlemefs45eN  37566  cdleme32c  37578  cdleme32e  37580  cdleme35h  37591  cdleme36a  37595  cdleme36m  37596  cdleme37m  37597  cdleme41sn3aw  37609  cdleme41sn4aw  37610  cdleme41fva11  37612  cdleme42k  37619  cdleme43cN  37626  cdleme43dN  37627  cdleme46f2g1  37629  cdlemeg47rv2  37645  cdlemeg46sfg  37655  cdlemeg46fjgN  37656  cdlemeg46rjgN  37657  cdlemeg46fjv  37658  cdlemeg46frv  37660  cdlemeg46vrg  37662  cdlemeg46rgv  37663  cdlemeg46req  37664  cdlemeg46gfv  37665  cdleme50trn2a  37685  cdlemg2fv2  37735  cdlemg4a  37743  cdlemg4e  37749  cdlemg4f  37750  cdlemg8b  37763  cdlemg8c  37764  cdlemg9a  37767  cdlemg9b  37768  cdlemg9  37769  cdlemg10a  37775  cdlemg12a  37778  cdlemg12b  37779  cdlemg12c  37780  cdlemg12  37785  cdlemg17dN  37798  cdlemg17dALTN  37799  cdlemg17e  37800  cdlemg17i  37804  cdlemg17ir  37805  cdlemg17pq  37807  cdlemg17bq  37808  cdlemg17iqN  37809  cdlemg17  37812  cdlemg18b  37814  cdlemg18c  37815  cdlemg18d  37816  cdlemg18  37817  cdlemg19  37819  cdlemg21  37821  cdlemg28a  37828  cdlemg31b0a  37830  cdlemg33b0  37836  cdlemg35  37848  cdlemg44a  37866  cdlemh  37952  cdlemi2  37954  cdlemj1  37956  cdlemk5a  37970  cdlemk5  37971  cdlemki  37976  cdlemkvcl  37977  cdlemk10  37978  cdlemksv2  37982  cdlemk7  37983  cdlemk11  37984  cdlemk12  37985  cdlemk15  37990  cdlemk16a  37991  cdlemk16  37992  cdlemk5u  37996  cdlemk6u  37997  cdlemk18  38003  cdlemk19  38004  cdlemk7u  38005  cdlemk11u  38006  cdlemk12u  38007  cdlemk21N  38008  cdlemk20  38009  cdlemkoatnle-2N  38010  cdlemk13-2N  38011  cdlemkole-2N  38012  cdlemk14-2N  38013  cdlemk15-2N  38014  cdlemk16-2N  38015  cdlemk17-2N  38016  cdlemk18-2N  38021  cdlemk19-2N  38022  cdlemk22  38028  cdlemk30  38029  cdlemk28-3  38043  cdlemk33N  38044  cdlemkfid1N  38056  cdlemkid1  38057  cdlemky  38061  cdlemk11ta  38064  cdlemk35s-id  38073  cdlemk39s-id  38075  cdlemk47  38084  cdlemk48  38085  cdlemk49  38086  cdlemk50  38087  cdlemk51  38088  cdlemk52  38089  cdlemk53a  38090  cdlemk53b  38091  cdlemk53  38092  cdlemk54  38093  cdlemk55a  38094  cdlemkyyN  38097  cdlemk43N  38098  cdlemk55u1  38100  cdlemk55u  38101  cdlemk39u1  38102  cdlemk19u1  38104  cdleml1N  38111  cdleml2N  38112  cdleml3N  38113  dia2dimlem6  38204  cdlemn2  38330  cdlemn2a  38331  cdlemn5pre  38335  cdlemn11pre  38345  dihjustlem  38351  dihjust  38352  dihmeetlem15N  38456  lclkrlem2y  38666  relexpxpnnidm  40046