Theorem simp23 1089

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl23  1134  simpr23  1143  simp123  1188  simp223  1197  simp323  1206  funtpgOLD  5857  omeulem1  7549  elfiun  8219  cofsmo  8974  modexp  12861  iscatd2  16165  funcoppc  16358  funcres  16379  catcisolem  16579  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  pmtrprfv3  17697  mdetunilem3  20239  mdetunilem4  20240  mdetuni0  20246  mdetmul  20248  prdsxmetlem  21983  isosctrlem3  24350  isosctr  24351  f1otrg  25551  colinearalg  25590  ax5seglem6  25614  ax5seg  25618  axpasch  25621  axeuclid  25643  ogrpsub  29048  ogrpsublt  29053  rhmdvd  29152  bnj966  30268  bnj967  30269  mclspps  30735  cgrtr  31269  cgrtr3  31271  ofscom  31284  btwnxfr  31333  colinearxfr  31352  lineext  31353  brofs2  31354  brifs2  31355  fscgr  31357  linecgr  31358  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  seglecgr12im  31387  seglecgr12  31388  segletr  31391  broutsideof3  31403  outsideofeq  31407  lineunray  31424  eqlkr  33404  omlmod1i2N  33565  cvrcmp2  33589  cvlexch2  33634  cvlexchb2  33636  cvlatexchb2  33640  cvlatexch1  33641  cvlatexch2  33642  cvlatexch3  33643  cvlsupr7  33653  cvlsupr8  33654  atnlej1  33683  atnlej2  33684  2llnneN  33713  cvratlem  33725  atcvrneN  33734  atcvrj1  33735  atlelt  33742  2atjm  33749  3noncolr2  33753  3noncolr1N  33754  hlatcon2  33756  3dimlem2  33763  3dim1  33771  3dim2  33772  1cvrat  33780  ps-1  33781  ps-2  33782  2atjlej  33783  hlatexch3N  33784  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem6  33792  llnle  33822  2atm  33831  ps-2c  33832  lplni2  33841  lplnle  33844  lplnnle2at  33845  lplnri3N  33859  llncvrlpln2  33861  2atmat  33865  2llnjaN  33870  2llnm2N  33872  2llnm4  33874  2llnmeqat  33875  lvolnle3at  33886  4atlem0ae  33898  4atlem0be  33899  4atlem3b  33902  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem12a  33914  4at  33917  4at2  33918  lplncvrlvol2  33919  2lplnm2N  33925  2llnma1b  34090  2llnma1  34091  2llnma3r  34092  2llnma2  34093  2llnma2rN  34094  cdlema1N  34095  cdlema2N  34096  paddasslem2  34125  paddasslem15  34138  paddasslem16  34139  pmodlem1  34150  pmod2iN  34153  hlmod1i  34160  atmod2i1  34165  atmod2i2  34166  atmod3i1  34168  atmod3i2  34169  atmod4i1  34170  atmod4i2  34171  llnexchb2  34173  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem13  34187  dalawlem15  34189  osumcllem7N  34266  osumcllem9N  34268  osumcllem11N  34270  pl42lem1N  34283  4atex  34380  4atex2-0aOLDN  34382  4atex2-0bOLDN  34383  4atex2-0cOLDN  34384  trlval4  34493  cdlemc5  34500  cdlemd5  34507  cdlemd6  34508  cdleme00a  34514  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme16aN  34564  cdleme11c  34566  cdleme11g  34570  cdleme11h  34571  cdleme12  34576  cdleme0nex  34595  cdleme18a  34596  cdleme18b  34597  cdleme18c  34598  cdleme18d  34600  cdleme20zN  34606  cdleme20y  34607  cdleme20yOLD  34608  cdleme19a  34609  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20aN  34615  cdleme20c  34617  cdleme20d  34618  cdleme20i  34623  cdleme20j  34624  cdleme20l1  34626  cdleme20l2  34627  cdleme20m  34629  cdleme21b  34632  cdleme21c  34633  cdleme21j  34642  cdleme22aa  34645  cdleme22a  34646  cdleme22eALTN  34651  cdleme26e  34665  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme27N  34675  cdleme28a  34676  cdleme28b  34677  cdleme30a  34684  cdlemefs45eN  34737  cdleme32c  34749  cdleme32e  34751  cdleme35h  34762  cdleme36a  34766  cdleme36m  34767  cdleme37m  34768  cdleme41sn3aw  34780  cdleme41sn4aw  34781  cdleme41fva11  34783  cdleme42k  34790  cdleme43cN  34797  cdleme43dN  34798  cdleme46f2g1  34800  cdlemeg47rv2  34816  cdlemeg46sfg  34826  cdlemeg46fjgN  34827  cdlemeg46rjgN  34828  cdlemeg46fjv  34829  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdleme50trn2a  34856  cdlemg2fv2  34906  cdlemg4a  34914  cdlemg4e  34920  cdlemg4f  34921  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9b  34939  cdlemg9  34940  cdlemg10a  34946  cdlemg12a  34949  cdlemg12b  34950  cdlemg12c  34951  cdlemg12  34956  cdlemg17dN  34969  cdlemg17dALTN  34970  cdlemg17e  34971  cdlemg17i  34975  cdlemg17ir  34976  cdlemg17pq  34978  cdlemg17bq  34979  cdlemg17iqN  34980  cdlemg17  34983  cdlemg18b  34985  cdlemg18c  34986  cdlemg18d  34987  cdlemg18  34988  cdlemg19  34990  cdlemg21  34992  cdlemg28a  34999  cdlemg31b0a  35001  cdlemg33b0  35007  cdlemg35  35019  cdlemg44a  35037  cdlemh  35123  cdlemi2  35125  cdlemj1  35127  cdlemk5a  35141  cdlemk5  35142  cdlemki  35147  cdlemkvcl  35148  cdlemk10  35149  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemk15  35161  cdlemk16a  35162  cdlemk16  35163  cdlemk5u  35167  cdlemk6u  35168  cdlemk18  35174  cdlemk19  35175  cdlemk7u  35176  cdlemk11u  35177  cdlemk12u  35178  cdlemk21N  35179  cdlemk20  35180  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk22  35199  cdlemk30  35200  cdlemk28-3  35214  cdlemk33N  35215  cdlemkfid1N  35227  cdlemkid1  35228  cdlemky  35232  cdlemk11ta  35235  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk47  35255  cdlemk48  35256  cdlemk49  35257  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk53a  35261  cdlemk53b  35262  cdlemk53  35263  cdlemk54  35264  cdlemk55a  35265  cdlemkyyN  35268  cdlemk43N  35269  cdlemk55u1  35271  cdlemk55u  35272  cdlemk39u1  35273  cdlemk19u1  35275  cdleml1N  35282  cdleml2N  35283  cdleml3N  35284  dia2dimlem6  35376  cdlemn2  35502  cdlemn2a  35503  cdlemn5pre  35507  cdlemn11pre  35517  dihjustlem  35523  dihjust  35524  dihmeetlem15N  35628  lclkrlem2y  35838  relexpxpnnidm  37014  uhgr2edg  40435