Theorem simp23 1207

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  simp123  1306  simp223  1315  simp323  1324  omeulem1  8422  elfiun  9198  ttrclselem2  9493  cofsmo  10034  modexp  13962  iscatd2  17399  funcoppc  17599  funcres  17620  catcisolem  17834  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlfcl  17949  curf1cl  17955  curfcl  17959  hofcl  17986  pmtrprfv3  19071  mdetunilem3  21772  mdetunilem4  21773  mdetuni0  21779  mdetmul  21781  prdsxmetlem  23530  isosctrlem3  25979  isosctr  25980  f1otrg  27241  colinearalg  27287  ax5seglem6  27311  ax5seg  27315  axpasch  27318  axeuclid  27340  uhgr2edg  27584  clwwlkccat  28363  ogrpsub  31351  ogrpsublt  31356  rhmdvd  31529  bnj966  32933  bnj967  32934  mclspps  33555  noinfbnd2lem1  33942  cgrtr  34303  cgrtr3  34305  ofscom  34318  btwnxfr  34367  colinearxfr  34386  lineext  34387  brofs2  34388  brifs2  34389  fscgr  34391  linecgr  34392  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem7  34404  seglecgr12im  34421  seglecgr12  34422  segletr  34425  broutsideof3  34437  outsideofeq  34441  lineunray  34458  eqlkr  37120  omlmod1i2N  37281  cvrcmp2  37305  cvlexch2  37350  cvlexchb2  37352  cvlatexchb2  37356  cvlatexch1  37357  cvlatexch2  37358  cvlatexch3  37359  cvlsupr7  37369  cvlsupr8  37370  atnlej1  37400  atnlej2  37401  2llnneN  37430  cvratlem  37442  atcvrneN  37451  atcvrj1  37452  atlelt  37459  2atjm  37466  3noncolr2  37470  3noncolr1N  37471  hlatcon2  37473  3dimlem2  37480  3dim1  37488  3dim2  37489  1cvrat  37497  ps-1  37498  ps-2  37499  2atjlej  37500  hlatexch3N  37501  ps-2b  37503  3atlem1  37504  3atlem2  37505  3atlem6  37509  llnle  37539  2atm  37548  ps-2c  37549  lplni2  37558  lplnle  37561  lplnnle2at  37562  lplnri3N  37576  llncvrlpln2  37578  2atmat  37582  2llnjaN  37587  2llnm2N  37589  2llnm4  37591  2llnmeqat  37592  lvolnle3at  37603  4atlem0ae  37615  4atlem0be  37616  4atlem3b  37619  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem12a  37631  4at  37634  4at2  37635  lplncvrlvol2  37636  2lplnm2N  37642  2llnma1b  37807  2llnma1  37808  2llnma3r  37809  2llnma2  37810  2llnma2rN  37811  cdlema1N  37812  cdlema2N  37813  paddasslem2  37842  paddasslem15  37855  paddasslem16  37856  pmodlem1  37867  pmod2iN  37870  hlmod1i  37877  atmod2i1  37882  atmod2i2  37883  atmod3i1  37885  atmod3i2  37886  atmod4i1  37887  atmod4i2  37888  llnexchb2  37890  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem13  37904  dalawlem15  37906  osumcllem7N  37983  osumcllem9N  37985  osumcllem11N  37987  pl42lem1N  38000  4atex  38097  4atex2-0aOLDN  38099  4atex2-0bOLDN  38100  4atex2-0cOLDN  38101  trlval4  38209  cdlemc5  38216  cdlemd5  38223  cdlemd6  38224  cdleme00a  38230  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4  38259  cdleme4a  38260  cdleme16aN  38280  cdleme11c  38282  cdleme11g  38286  cdleme11h  38287  cdleme12  38292  cdleme0nex  38311  cdleme18a  38312  cdleme18b  38313  cdleme18c  38314  cdleme18d  38316  cdleme20zN  38322  cdleme20y  38323  cdleme19a  38324  cdleme19b  38325  cdleme19d  38327  cdleme19e  38328  cdleme20aN  38330  cdleme20c  38332  cdleme20d  38333  cdleme20i  38338  cdleme20j  38339  cdleme20l1  38341  cdleme20l2  38342  cdleme20m  38344  cdleme21b  38347  cdleme21c  38348  cdleme21j  38357  cdleme22aa  38360  cdleme22a  38361  cdleme22eALTN  38366  cdleme26e  38380  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme27N  38390  cdleme28a  38391  cdleme28b  38392  cdleme30a  38399  cdlemefs45eN  38452  cdleme32c  38464  cdleme32e  38466  cdleme35h  38477  cdleme36a  38481  cdleme36m  38482  cdleme37m  38483  cdleme41sn3aw  38495  cdleme41sn4aw  38496  cdleme41fva11  38498  cdleme42k  38505  cdleme43cN  38512  cdleme43dN  38513  cdleme46f2g1  38515  cdlemeg47rv2  38531  cdlemeg46sfg  38541  cdlemeg46fjgN  38542  cdlemeg46rjgN  38543  cdlemeg46fjv  38544  cdlemeg46frv  38546  cdlemeg46vrg  38548  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdleme50trn2a  38571  cdlemg2fv2  38621  cdlemg4a  38629  cdlemg4e  38635  cdlemg4f  38636  cdlemg8b  38649  cdlemg8c  38650  cdlemg9a  38653  cdlemg9b  38654  cdlemg9  38655  cdlemg10a  38661  cdlemg12a  38664  cdlemg12b  38665  cdlemg12c  38666  cdlemg12  38671  cdlemg17dN  38684  cdlemg17dALTN  38685  cdlemg17e  38686  cdlemg17i  38690  cdlemg17ir  38691  cdlemg17pq  38693  cdlemg17bq  38694  cdlemg17iqN  38695  cdlemg17  38698  cdlemg18b  38700  cdlemg18c  38701  cdlemg18d  38702  cdlemg18  38703  cdlemg19  38705  cdlemg21  38707  cdlemg28a  38714  cdlemg31b0a  38716  cdlemg33b0  38722  cdlemg35  38734  cdlemg44a  38752  cdlemh  38838  cdlemi2  38840  cdlemj1  38842  cdlemk5a  38856  cdlemk5  38857  cdlemki  38862  cdlemkvcl  38863  cdlemk10  38864  cdlemksv2  38868  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemk15  38876  cdlemk16a  38877  cdlemk16  38878  cdlemk5u  38882  cdlemk6u  38883  cdlemk18  38889  cdlemk19  38890  cdlemk7u  38891  cdlemk11u  38892  cdlemk12u  38893  cdlemk21N  38894  cdlemk20  38895  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk22  38914  cdlemk30  38915  cdlemk28-3  38929  cdlemk33N  38930  cdlemkfid1N  38942  cdlemkid1  38943  cdlemky  38947  cdlemk11ta  38950  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk47  38970  cdlemk48  38971  cdlemk49  38972  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk53a  38976  cdlemk53b  38977  cdlemk53  38978  cdlemk54  38979  cdlemk55a  38980  cdlemkyyN  38983  cdlemk43N  38984  cdlemk55u1  38986  cdlemk55u  38987  cdlemk39u1  38988  cdlemk19u1  38990  cdleml1N  38997  cdleml2N  38998  cdleml3N  38999  dia2dimlem6  39090  cdlemn2  39216  cdlemn2a  39217  cdlemn5pre  39221  cdlemn11pre  39231  dihjustlem  39237  dihjust  39238  dihmeetlem15N  39342  lclkrlem2y  39552  relexpxpnnidm  41318  iscnrm3llem1  46254  iscnrm3l  46256  natglobalincr  46523