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 1138	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant2 1134	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8509  elfiun  9333  ttrclselem2  9635  cofsmo  10179  modexp  14161  iscatd2  17604  funcoppc  17799  funcres  17820  catcisolem  18034  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlfcl  18145  curf1cl  18151  curfcl  18155  hofcl  18182  pmtrprfv3  19383  ogrpsub  20066  ogrpsublt  20071  mdetunilem3  22558  mdetunilem4  22559  mdetuni0  22565  mdetmul  22567  prdsxmetlem  24312  isosctrlem3  26786  isosctr  26787  noinfbnd2lem1  27698  addsass  28001  f1otrg  28943  colinearalg  28983  ax5seglem6  29007  ax5seg  29011  axpasch  29014  axeuclid  29036  uhgr2edg  29281  clwwlkccat  30065  rhmdvd  33405  bnj966  35100  bnj967  35101  mclspps  35778  cgrtr  36186  cgrtr3  36188  ofscom  36201  btwnxfr  36250  colinearxfr  36269  lineext  36270  brofs2  36271  brifs2  36272  fscgr  36274  linecgr  36275  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  seglecgr12im  36304  seglecgr12  36305  segletr  36308  broutsideof3  36320  outsideofeq  36324  lineunray  36341  eqlkr  39359  omlmod1i2N  39520  cvrcmp2  39544  cvlexch2  39589  cvlexchb2  39591  cvlatexchb2  39595  cvlatexch1  39596  cvlatexch2  39597  cvlatexch3  39598  cvlsupr7  39608  cvlsupr8  39609  atnlej1  39639  atnlej2  39640  2llnneN  39669  cvratlem  39681  atcvrneN  39690  atcvrj1  39691  atlelt  39698  2atjm  39705  3noncolr2  39709  3noncolr1N  39710  hlatcon2  39712  3dimlem2  39719  3dim1  39727  3dim2  39728  1cvrat  39736  ps-1  39737  ps-2  39738  2atjlej  39739  hlatexch3N  39740  ps-2b  39742  3atlem1  39743  3atlem2  39744  3atlem6  39748  llnle  39778  2atm  39787  ps-2c  39788  lplni2  39797  lplnle  39800  lplnnle2at  39801  lplnri3N  39815  llncvrlpln2  39817  2atmat  39821  2llnjaN  39826  2llnm2N  39828  2llnm4  39830  2llnmeqat  39831  lvolnle3at  39842  4atlem0ae  39854  4atlem0be  39855  4atlem3b  39858  4atlem9  39863  4atlem10a  39864  4atlem10  39866  4atlem11a  39867  4atlem12a  39870  4at  39873  4at2  39874  lplncvrlvol2  39875  2lplnm2N  39881  2llnma1b  40046  2llnma1  40047  2llnma3r  40048  2llnma2  40049  2llnma2rN  40050  cdlema1N  40051  cdlema2N  40052  paddasslem2  40081  paddasslem15  40094  paddasslem16  40095  pmodlem1  40106  pmod2iN  40109  hlmod1i  40116  atmod2i1  40121  atmod2i2  40122  atmod3i1  40124  atmod3i2  40125  atmod4i1  40126  atmod4i2  40127  llnexchb2  40129  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem11  40141  dalawlem13  40143  dalawlem15  40145  osumcllem7N  40222  osumcllem9N  40224  osumcllem11N  40226  pl42lem1N  40239  4atex  40336  4atex2-0aOLDN  40338  4atex2-0bOLDN  40339  4atex2-0cOLDN  40340  trlval4  40448  cdlemc5  40455  cdlemd5  40462  cdlemd6  40463  cdleme00a  40469  cdleme3g  40494  cdleme3h  40495  cdleme3  40497  cdleme4  40498  cdleme4a  40499  cdleme16aN  40519  cdleme11c  40521  cdleme11g  40525  cdleme11h  40526  cdleme12  40531  cdleme0nex  40550  cdleme18a  40551  cdleme18b  40552  cdleme18c  40553  cdleme18d  40555  cdleme20zN  40561  cdleme20y  40562  cdleme19a  40563  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20aN  40569  cdleme20c  40571  cdleme20d  40572  cdleme20i  40577  cdleme20j  40578  cdleme20l1  40580  cdleme20l2  40581  cdleme20m  40583  cdleme21b  40586  cdleme21c  40587  cdleme21j  40596  cdleme22aa  40599  cdleme22a  40600  cdleme22eALTN  40605  cdleme26e  40619  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme27N  40629  cdleme28a  40630  cdleme28b  40631  cdleme30a  40638  cdlemefs45eN  40691  cdleme32c  40703  cdleme32e  40705  cdleme35h  40716  cdleme36a  40720  cdleme36m  40721  cdleme37m  40722  cdleme41sn3aw  40734  cdleme41sn4aw  40735  cdleme41fva11  40737  cdleme42k  40744  cdleme43cN  40751  cdleme43dN  40752  cdleme46f2g1  40754  cdlemeg47rv2  40770  cdlemeg46sfg  40780  cdlemeg46fjgN  40781  cdlemeg46rjgN  40782  cdlemeg46fjv  40783  cdlemeg46frv  40785  cdlemeg46vrg  40787  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemeg46gfv  40790  cdleme50trn2a  40810  cdlemg2fv2  40860  cdlemg4a  40868  cdlemg4e  40874  cdlemg4f  40875  cdlemg8b  40888  cdlemg8c  40889  cdlemg9a  40892  cdlemg9b  40893  cdlemg9  40894  cdlemg10a  40900  cdlemg12a  40903  cdlemg12b  40904  cdlemg12c  40905  cdlemg12  40910  cdlemg17dN  40923  cdlemg17dALTN  40924  cdlemg17e  40925  cdlemg17i  40929  cdlemg17ir  40930  cdlemg17pq  40932  cdlemg17bq  40933  cdlemg17iqN  40934  cdlemg17  40937  cdlemg18b  40939  cdlemg18c  40940  cdlemg18d  40941  cdlemg18  40942  cdlemg19  40944  cdlemg21  40946  cdlemg28a  40953  cdlemg31b0a  40955  cdlemg33b0  40961  cdlemg35  40973  cdlemg44a  40991  cdlemh  41077  cdlemi2  41079  cdlemj1  41081  cdlemk5a  41095  cdlemk5  41096  cdlemki  41101  cdlemkvcl  41102  cdlemk10  41103  cdlemksv2  41107  cdlemk7  41108  cdlemk11  41109  cdlemk12  41110  cdlemk15  41115  cdlemk16a  41116  cdlemk16  41117  cdlemk5u  41121  cdlemk6u  41122  cdlemk18  41128  cdlemk19  41129  cdlemk7u  41130  cdlemk11u  41131  cdlemk12u  41132  cdlemk21N  41133  cdlemk20  41134  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk22  41153  cdlemk30  41154  cdlemk28-3  41168  cdlemk33N  41169  cdlemkfid1N  41181  cdlemkid1  41182  cdlemky  41186  cdlemk11ta  41189  cdlemk35s-id  41198  cdlemk39s-id  41200  cdlemk47  41209  cdlemk48  41210  cdlemk49  41211  cdlemk50  41212  cdlemk51  41213  cdlemk52  41214  cdlemk53a  41215  cdlemk53b  41216  cdlemk53  41217  cdlemk54  41218  cdlemk55a  41219  cdlemkyyN  41222  cdlemk43N  41223  cdlemk55u1  41225  cdlemk55u  41226  cdlemk39u1  41227  cdlemk19u1  41229  cdleml1N  41236  cdleml2N  41237  cdleml3N  41238  dia2dimlem6  41329  cdlemn2  41455  cdlemn2a  41456  cdlemn5pre  41460  cdlemn11pre  41470  dihjustlem  41476  dihjust  41477  dihmeetlem15N  41581  lclkrlem2y  41791  relexpxpnnidm  43944  ormkglobd  47119  natglobalincr  47121  iscnrm3llem1  49194  iscnrm3l  49196  swapffunc  49527  fucofunc  49604