Theorem simp23 1208

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 1087

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 1089

This theorem is referenced by:  simp123  1307  simp223  1316  simp323  1325  omeulem1  8581  elfiun  9424  ttrclselem2  9720  cofsmo  10263  modexp  14200  iscatd2  17624  funcoppc  17824  funcres  17845  catcisolem  18059  1stfcl  18148  2ndfcl  18149  prfcl  18154  evlfcl  18174  curf1cl  18180  curfcl  18184  hofcl  18211  pmtrprfv3  19321  mdetunilem3  22115  mdetunilem4  22116  mdetuni0  22122  mdetmul  22124  prdsxmetlem  23873  isosctrlem3  26322  isosctr  26323  noinfbnd2lem1  27230  addsass  27485  f1otrg  28119  colinearalg  28165  ax5seglem6  28189  ax5seg  28193  axpasch  28196  axeuclid  28218  uhgr2edg  28462  clwwlkccat  29240  ogrpsub  32229  ogrpsublt  32234  rhmdvd  32431  bnj966  33950  bnj967  33951  mclspps  34570  cgrtr  34959  cgrtr3  34961  ofscom  34974  btwnxfr  35023  colinearxfr  35042  lineext  35043  brofs2  35044  brifs2  35045  fscgr  35047  linecgr  35048  btwnconn1lem1  35054  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem7  35060  seglecgr12im  35077  seglecgr12  35078  segletr  35081  broutsideof3  35093  outsideofeq  35097  lineunray  35114  eqlkr  37964  omlmod1i2N  38125  cvrcmp2  38149  cvlexch2  38194  cvlexchb2  38196  cvlatexchb2  38200  cvlatexch1  38201  cvlatexch2  38202  cvlatexch3  38203  cvlsupr7  38213  cvlsupr8  38214  atnlej1  38245  atnlej2  38246  2llnneN  38275  cvratlem  38287  atcvrneN  38296  atcvrj1  38297  atlelt  38304  2atjm  38311  3noncolr2  38315  3noncolr1N  38316  hlatcon2  38318  3dimlem2  38325  3dim1  38333  3dim2  38334  1cvrat  38342  ps-1  38343  ps-2  38344  2atjlej  38345  hlatexch3N  38346  ps-2b  38348  3atlem1  38349  3atlem2  38350  3atlem6  38354  llnle  38384  2atm  38393  ps-2c  38394  lplni2  38403  lplnle  38406  lplnnle2at  38407  lplnri3N  38421  llncvrlpln2  38423  2atmat  38427  2llnjaN  38432  2llnm2N  38434  2llnm4  38436  2llnmeqat  38437  lvolnle3at  38448  4atlem0ae  38460  4atlem0be  38461  4atlem3b  38464  4atlem9  38469  4atlem10a  38470  4atlem10  38472  4atlem11a  38473  4atlem12a  38476  4at  38479  4at2  38480  lplncvrlvol2  38481  2lplnm2N  38487  2llnma1b  38652  2llnma1  38653  2llnma3r  38654  2llnma2  38655  2llnma2rN  38656  cdlema1N  38657  cdlema2N  38658  paddasslem2  38687  paddasslem15  38700  paddasslem16  38701  pmodlem1  38712  pmod2iN  38715  hlmod1i  38722  atmod2i1  38727  atmod2i2  38728  atmod3i1  38730  atmod3i2  38731  atmod4i1  38732  atmod4i2  38733  llnexchb2  38735  dalawlem3  38739  dalawlem4  38740  dalawlem5  38741  dalawlem6  38742  dalawlem7  38743  dalawlem8  38744  dalawlem9  38745  dalawlem11  38747  dalawlem13  38749  dalawlem15  38751  osumcllem7N  38828  osumcllem9N  38830  osumcllem11N  38832  pl42lem1N  38845  4atex  38942  4atex2-0aOLDN  38944  4atex2-0bOLDN  38945  4atex2-0cOLDN  38946  trlval4  39054  cdlemc5  39061  cdlemd5  39068  cdlemd6  39069  cdleme00a  39075  cdleme3g  39100  cdleme3h  39101  cdleme3  39103  cdleme4  39104  cdleme4a  39105  cdleme16aN  39125  cdleme11c  39127  cdleme11g  39131  cdleme11h  39132  cdleme12  39137  cdleme0nex  39156  cdleme18a  39157  cdleme18b  39158  cdleme18c  39159  cdleme18d  39161  cdleme20zN  39167  cdleme20y  39168  cdleme19a  39169  cdleme19b  39170  cdleme19d  39172  cdleme19e  39173  cdleme20aN  39175  cdleme20c  39177  cdleme20d  39178  cdleme20i  39183  cdleme20j  39184  cdleme20l1  39186  cdleme20l2  39187  cdleme20m  39189  cdleme21b  39192  cdleme21c  39193  cdleme21j  39202  cdleme22aa  39205  cdleme22a  39206  cdleme22eALTN  39211  cdleme26e  39225  cdleme26fALTN  39228  cdleme26f  39229  cdleme26f2ALTN  39230  cdleme26f2  39231  cdleme27N  39235  cdleme28a  39236  cdleme28b  39237  cdleme30a  39244  cdlemefs45eN  39297  cdleme32c  39309  cdleme32e  39311  cdleme35h  39322  cdleme36a  39326  cdleme36m  39327  cdleme37m  39328  cdleme41sn3aw  39340  cdleme41sn4aw  39341  cdleme41fva11  39343  cdleme42k  39350  cdleme43cN  39357  cdleme43dN  39358  cdleme46f2g1  39360  cdlemeg47rv2  39376  cdlemeg46sfg  39386  cdlemeg46fjgN  39387  cdlemeg46rjgN  39388  cdlemeg46fjv  39389  cdlemeg46frv  39391  cdlemeg46vrg  39393  cdlemeg46rgv  39394  cdlemeg46req  39395  cdlemeg46gfv  39396  cdleme50trn2a  39416  cdlemg2fv2  39466  cdlemg4a  39474  cdlemg4e  39480  cdlemg4f  39481  cdlemg8b  39494  cdlemg8c  39495  cdlemg9a  39498  cdlemg9b  39499  cdlemg9  39500  cdlemg10a  39506  cdlemg12a  39509  cdlemg12b  39510  cdlemg12c  39511  cdlemg12  39516  cdlemg17dN  39529  cdlemg17dALTN  39530  cdlemg17e  39531  cdlemg17i  39535  cdlemg17ir  39536  cdlemg17pq  39538  cdlemg17bq  39539  cdlemg17iqN  39540  cdlemg17  39543  cdlemg18b  39545  cdlemg18c  39546  cdlemg18d  39547  cdlemg18  39548  cdlemg19  39550  cdlemg21  39552  cdlemg28a  39559  cdlemg31b0a  39561  cdlemg33b0  39567  cdlemg35  39579  cdlemg44a  39597  cdlemh  39683  cdlemi2  39685  cdlemj1  39687  cdlemk5a  39701  cdlemk5  39702  cdlemki  39707  cdlemkvcl  39708  cdlemk10  39709  cdlemksv2  39713  cdlemk7  39714  cdlemk11  39715  cdlemk12  39716  cdlemk15  39721  cdlemk16a  39722  cdlemk16  39723  cdlemk5u  39727  cdlemk6u  39728  cdlemk18  39734  cdlemk19  39735  cdlemk7u  39736  cdlemk11u  39737  cdlemk12u  39738  cdlemk21N  39739  cdlemk20  39740  cdlemkoatnle-2N  39741  cdlemk13-2N  39742  cdlemkole-2N  39743  cdlemk14-2N  39744  cdlemk15-2N  39745  cdlemk16-2N  39746  cdlemk17-2N  39747  cdlemk18-2N  39752  cdlemk19-2N  39753  cdlemk22  39759  cdlemk30  39760  cdlemk28-3  39774  cdlemk33N  39775  cdlemkfid1N  39787  cdlemkid1  39788  cdlemky  39792  cdlemk11ta  39795  cdlemk35s-id  39804  cdlemk39s-id  39806  cdlemk47  39815  cdlemk48  39816  cdlemk49  39817  cdlemk50  39818  cdlemk51  39819  cdlemk52  39820  cdlemk53a  39821  cdlemk53b  39822  cdlemk53  39823  cdlemk54  39824  cdlemk55a  39825  cdlemkyyN  39828  cdlemk43N  39829  cdlemk55u1  39831  cdlemk55u  39832  cdlemk39u1  39833  cdlemk19u1  39835  cdleml1N  39842  cdleml2N  39843  cdleml3N  39844  dia2dimlem6  39935  cdlemn2  40061  cdlemn2a  40062  cdlemn5pre  40066  cdlemn11pre  40076  dihjustlem  40082  dihjust  40083  dihmeetlem15N  40187  lclkrlem2y  40397  relexpxpnnidm  42444  natglobalincr  45581  iscnrm3llem1  47572  iscnrm3l  47574