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

This theorem is referenced by:  simp123  1306  simp223  1315  simp323  1324  omeulem1  8618  elfiun  9467  ttrclselem2  9763  cofsmo  10306  modexp  14273  iscatd2  17725  funcoppc  17925  funcres  17946  catcisolem  18163  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  pmtrprfv3  19486  mdetunilem3  22635  mdetunilem4  22636  mdetuni0  22642  mdetmul  22644  prdsxmetlem  24393  isosctrlem3  26877  isosctr  26878  noinfbnd2lem1  27789  addsass  28052  f1otrg  28893  colinearalg  28939  ax5seglem6  28963  ax5seg  28967  axpasch  28970  axeuclid  28992  uhgr2edg  29239  clwwlkccat  30018  ogrpsub  33075  ogrpsublt  33080  rhmdvd  33327  bnj966  34936  bnj967  34937  mclspps  35568  cgrtr  35973  cgrtr3  35975  ofscom  35988  btwnxfr  36037  colinearxfr  36056  lineext  36057  brofs2  36058  brifs2  36059  fscgr  36061  linecgr  36062  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem7  36074  seglecgr12im  36091  seglecgr12  36092  segletr  36095  broutsideof3  36107  outsideofeq  36111  lineunray  36128  eqlkr  39080  omlmod1i2N  39241  cvrcmp2  39265  cvlexch2  39310  cvlexchb2  39312  cvlatexchb2  39316  cvlatexch1  39317  cvlatexch2  39318  cvlatexch3  39319  cvlsupr7  39329  cvlsupr8  39330  atnlej1  39361  atnlej2  39362  2llnneN  39391  cvratlem  39403  atcvrneN  39412  atcvrj1  39413  atlelt  39420  2atjm  39427  3noncolr2  39431  3noncolr1N  39432  hlatcon2  39434  3dimlem2  39441  3dim1  39449  3dim2  39450  1cvrat  39458  ps-1  39459  ps-2  39460  2atjlej  39461  hlatexch3N  39462  ps-2b  39464  3atlem1  39465  3atlem2  39466  3atlem6  39470  llnle  39500  2atm  39509  ps-2c  39510  lplni2  39519  lplnle  39522  lplnnle2at  39523  lplnri3N  39537  llncvrlpln2  39539  2atmat  39543  2llnjaN  39548  2llnm2N  39550  2llnm4  39552  2llnmeqat  39553  lvolnle3at  39564  4atlem0ae  39576  4atlem0be  39577  4atlem3b  39580  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem12a  39592  4at  39595  4at2  39596  lplncvrlvol2  39597  2lplnm2N  39603  2llnma1b  39768  2llnma1  39769  2llnma3r  39770  2llnma2  39771  2llnma2rN  39772  cdlema1N  39773  cdlema2N  39774  paddasslem2  39803  paddasslem15  39816  paddasslem16  39817  pmodlem1  39828  pmod2iN  39831  hlmod1i  39838  atmod2i1  39843  atmod2i2  39844  atmod3i1  39846  atmod3i2  39847  atmod4i1  39848  atmod4i2  39849  llnexchb2  39851  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem13  39865  dalawlem15  39867  osumcllem7N  39944  osumcllem9N  39946  osumcllem11N  39948  pl42lem1N  39961  4atex  40058  4atex2-0aOLDN  40060  4atex2-0bOLDN  40061  4atex2-0cOLDN  40062  trlval4  40170  cdlemc5  40177  cdlemd5  40184  cdlemd6  40185  cdleme00a  40191  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme4a  40221  cdleme16aN  40241  cdleme11c  40243  cdleme11g  40247  cdleme11h  40248  cdleme12  40253  cdleme0nex  40272  cdleme18a  40273  cdleme18b  40274  cdleme18c  40275  cdleme18d  40277  cdleme20zN  40283  cdleme20y  40284  cdleme19a  40285  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20aN  40291  cdleme20c  40293  cdleme20d  40294  cdleme20i  40299  cdleme20j  40300  cdleme20l1  40302  cdleme20l2  40303  cdleme20m  40305  cdleme21b  40308  cdleme21c  40309  cdleme21j  40318  cdleme22aa  40321  cdleme22a  40322  cdleme22eALTN  40327  cdleme26e  40341  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme30a  40360  cdlemefs45eN  40413  cdleme32c  40425  cdleme32e  40427  cdleme35h  40438  cdleme36a  40442  cdleme36m  40443  cdleme37m  40444  cdleme41sn3aw  40456  cdleme41sn4aw  40457  cdleme41fva11  40459  cdleme42k  40466  cdleme43cN  40473  cdleme43dN  40474  cdleme46f2g1  40476  cdlemeg47rv2  40492  cdlemeg46sfg  40502  cdlemeg46fjgN  40503  cdlemeg46rjgN  40504  cdlemeg46fjv  40505  cdlemeg46frv  40507  cdlemeg46vrg  40509  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme50trn2a  40532  cdlemg2fv2  40582  cdlemg4a  40590  cdlemg4e  40596  cdlemg4f  40597  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg9b  40615  cdlemg9  40616  cdlemg10a  40622  cdlemg12a  40625  cdlemg12b  40626  cdlemg12c  40627  cdlemg12  40632  cdlemg17dN  40645  cdlemg17dALTN  40646  cdlemg17e  40647  cdlemg17i  40651  cdlemg17ir  40652  cdlemg17pq  40654  cdlemg17bq  40655  cdlemg17iqN  40656  cdlemg17  40659  cdlemg18b  40661  cdlemg18c  40662  cdlemg18d  40663  cdlemg18  40664  cdlemg19  40666  cdlemg21  40668  cdlemg28a  40675  cdlemg31b0a  40677  cdlemg33b0  40683  cdlemg35  40695  cdlemg44a  40713  cdlemh  40799  cdlemi2  40801  cdlemj1  40803  cdlemk5a  40817  cdlemk5  40818  cdlemki  40823  cdlemkvcl  40824  cdlemk10  40825  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemk15  40837  cdlemk16a  40838  cdlemk16  40839  cdlemk5u  40843  cdlemk6u  40844  cdlemk18  40850  cdlemk19  40851  cdlemk7u  40852  cdlemk11u  40853  cdlemk12u  40854  cdlemk21N  40855  cdlemk20  40856  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk22  40875  cdlemk30  40876  cdlemk28-3  40890  cdlemk33N  40891  cdlemkfid1N  40903  cdlemkid1  40904  cdlemky  40908  cdlemk11ta  40911  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk47  40931  cdlemk48  40932  cdlemk49  40933  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdlemk53b  40938  cdlemk53  40939  cdlemk54  40940  cdlemk55a  40941  cdlemkyyN  40944  cdlemk43N  40945  cdlemk55u1  40947  cdlemk55u  40948  cdlemk39u1  40949  cdlemk19u1  40951  cdleml1N  40958  cdleml2N  40959  cdleml3N  40960  dia2dimlem6  41051  cdlemn2  41177  cdlemn2a  41178  cdlemn5pre  41182  cdlemn11pre  41192  dihjustlem  41198  dihjust  41199  dihmeetlem15N  41303  lclkrlem2y  41513  relexpxpnnidm  43692  natglobalincr  46830  iscnrm3llem1  48745  iscnrm3l  48747