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  8506  elfiun  9325  ttrclselem2  9627  cofsmo  10171  modexp  14152  iscatd2  17595  funcoppc  17790  funcres  17811  catcisolem  18025  1stfcl  18111  2ndfcl  18112  prfcl  18117  evlfcl  18136  curf1cl  18142  curfcl  18146  hofcl  18173  pmtrprfv3  19374  ogrpsub  20057  ogrpsublt  20062  mdetunilem3  22549  mdetunilem4  22550  mdetuni0  22556  mdetmul  22558  prdsxmetlem  24303  isosctrlem3  26777  isosctr  26778  noinfbnd2lem1  27689  addsass  27968  f1otrg  28869  colinearalg  28909  ax5seglem6  28933  ax5seg  28937  axpasch  28940  axeuclid  28962  uhgr2edg  29207  clwwlkccat  29991  rhmdvd  33333  bnj966  35028  bnj967  35029  mclspps  35700  cgrtr  36108  cgrtr3  36110  ofscom  36123  btwnxfr  36172  colinearxfr  36191  lineext  36192  brofs2  36193  brifs2  36194  fscgr  36196  linecgr  36197  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem3  36205  btwnconn1lem4  36206  btwnconn1lem5  36207  btwnconn1lem6  36208  btwnconn1lem7  36209  seglecgr12im  36226  seglecgr12  36227  segletr  36230  broutsideof3  36242  outsideofeq  36246  lineunray  36263  eqlkr  39271  omlmod1i2N  39432  cvrcmp2  39456  cvlexch2  39501  cvlexchb2  39503  cvlatexchb2  39507  cvlatexch1  39508  cvlatexch2  39509  cvlatexch3  39510  cvlsupr7  39520  cvlsupr8  39521  atnlej1  39551  atnlej2  39552  2llnneN  39581  cvratlem  39593  atcvrneN  39602  atcvrj1  39603  atlelt  39610  2atjm  39617  3noncolr2  39621  3noncolr1N  39622  hlatcon2  39624  3dimlem2  39631  3dim1  39639  3dim2  39640  1cvrat  39648  ps-1  39649  ps-2  39650  2atjlej  39651  hlatexch3N  39652  ps-2b  39654  3atlem1  39655  3atlem2  39656  3atlem6  39660  llnle  39690  2atm  39699  ps-2c  39700  lplni2  39709  lplnle  39712  lplnnle2at  39713  lplnri3N  39727  llncvrlpln2  39729  2atmat  39733  2llnjaN  39738  2llnm2N  39740  2llnm4  39742  2llnmeqat  39743  lvolnle3at  39754  4atlem0ae  39766  4atlem0be  39767  4atlem3b  39770  4atlem9  39775  4atlem10a  39776  4atlem10  39778  4atlem11a  39779  4atlem12a  39782  4at  39785  4at2  39786  lplncvrlvol2  39787  2lplnm2N  39793  2llnma1b  39958  2llnma1  39959  2llnma3r  39960  2llnma2  39961  2llnma2rN  39962  cdlema1N  39963  cdlema2N  39964  paddasslem2  39993  paddasslem15  40006  paddasslem16  40007  pmodlem1  40018  pmod2iN  40021  hlmod1i  40028  atmod2i1  40033  atmod2i2  40034  atmod3i1  40036  atmod3i2  40037  atmod4i1  40038  atmod4i2  40039  llnexchb2  40041  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem13  40055  dalawlem15  40057  osumcllem7N  40134  osumcllem9N  40136  osumcllem11N  40138  pl42lem1N  40151  4atex  40248  4atex2-0aOLDN  40250  4atex2-0bOLDN  40251  4atex2-0cOLDN  40252  trlval4  40360  cdlemc5  40367  cdlemd5  40374  cdlemd6  40375  cdleme00a  40381  cdleme3g  40406  cdleme3h  40407  cdleme3  40409  cdleme4  40410  cdleme4a  40411  cdleme16aN  40431  cdleme11c  40433  cdleme11g  40437  cdleme11h  40438  cdleme12  40443  cdleme0nex  40462  cdleme18a  40463  cdleme18b  40464  cdleme18c  40465  cdleme18d  40467  cdleme20zN  40473  cdleme20y  40474  cdleme19a  40475  cdleme19b  40476  cdleme19d  40478  cdleme19e  40479  cdleme20aN  40481  cdleme20c  40483  cdleme20d  40484  cdleme20i  40489  cdleme20j  40490  cdleme20l1  40492  cdleme20l2  40493  cdleme20m  40495  cdleme21b  40498  cdleme21c  40499  cdleme21j  40508  cdleme22aa  40511  cdleme22a  40512  cdleme22eALTN  40517  cdleme26e  40531  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme27N  40541  cdleme28a  40542  cdleme28b  40543  cdleme30a  40550  cdlemefs45eN  40603  cdleme32c  40615  cdleme32e  40617  cdleme35h  40628  cdleme36a  40632  cdleme36m  40633  cdleme37m  40634  cdleme41sn3aw  40646  cdleme41sn4aw  40647  cdleme41fva11  40649  cdleme42k  40656  cdleme43cN  40663  cdleme43dN  40664  cdleme46f2g1  40666  cdlemeg47rv2  40682  cdlemeg46sfg  40692  cdlemeg46fjgN  40693  cdlemeg46rjgN  40694  cdlemeg46fjv  40695  cdlemeg46frv  40697  cdlemeg46vrg  40699  cdlemeg46rgv  40700  cdlemeg46req  40701  cdlemeg46gfv  40702  cdleme50trn2a  40722  cdlemg2fv2  40772  cdlemg4a  40780  cdlemg4e  40786  cdlemg4f  40787  cdlemg8b  40800  cdlemg8c  40801  cdlemg9a  40804  cdlemg9b  40805  cdlemg9  40806  cdlemg10a  40812  cdlemg12a  40815  cdlemg12b  40816  cdlemg12c  40817  cdlemg12  40822  cdlemg17dN  40835  cdlemg17dALTN  40836  cdlemg17e  40837  cdlemg17i  40841  cdlemg17ir  40842  cdlemg17pq  40844  cdlemg17bq  40845  cdlemg17iqN  40846  cdlemg17  40849  cdlemg18b  40851  cdlemg18c  40852  cdlemg18d  40853  cdlemg18  40854  cdlemg19  40856  cdlemg21  40858  cdlemg28a  40865  cdlemg31b0a  40867  cdlemg33b0  40873  cdlemg35  40885  cdlemg44a  40903  cdlemh  40989  cdlemi2  40991  cdlemj1  40993  cdlemk5a  41007  cdlemk5  41008  cdlemki  41013  cdlemkvcl  41014  cdlemk10  41015  cdlemksv2  41019  cdlemk7  41020  cdlemk11  41021  cdlemk12  41022  cdlemk15  41027  cdlemk16a  41028  cdlemk16  41029  cdlemk5u  41033  cdlemk6u  41034  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk11u  41043  cdlemk12u  41044  cdlemk21N  41045  cdlemk20  41046  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk22  41065  cdlemk30  41066  cdlemk28-3  41080  cdlemk33N  41081  cdlemkfid1N  41093  cdlemkid1  41094  cdlemky  41098  cdlemk11ta  41101  cdlemk35s-id  41110  cdlemk39s-id  41112  cdlemk47  41121  cdlemk48  41122  cdlemk49  41123  cdlemk50  41124  cdlemk51  41125  cdlemk52  41126  cdlemk53a  41127  cdlemk53b  41128  cdlemk53  41129  cdlemk54  41130  cdlemk55a  41131  cdlemkyyN  41134  cdlemk43N  41135  cdlemk55u1  41137  cdlemk55u  41138  cdlemk39u1  41139  cdlemk19u1  41141  cdleml1N  41148  cdleml2N  41149  cdleml3N  41150  dia2dimlem6  41241  cdlemn2  41367  cdlemn2a  41368  cdlemn5pre  41372  cdlemn11pre  41382  dihjustlem  41388  dihjust  41389  dihmeetlem15N  41493  lclkrlem2y  41703  relexpxpnnidm  43860  ormkglobd  47035  natglobalincr  47037  iscnrm3llem1  49110  iscnrm3l  49112  swapffunc  49443  fucofunc  49520