Theorem simp23 1215

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp123  1314  simp223  1323  simp323  1332  omeulem1  8514  elfiun  9340  ttrclselem2  9645  cofsmo  10189  modexp  14198  iscatd2  17645  funcoppc  17840  funcres  17861  catcisolem  18075  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  pmtrprfv3  19427  ogrpsub  20110  ogrpsublt  20115  mdetunilem3  22604  mdetunilem4  22605  mdetuni0  22611  mdetmul  22613  prdsxmetlem  24358  isosctrlem3  26809  isosctr  26810  noinfbnd2lem1  27719  addsass  28022  f1otrg  28964  colinearalg  29004  ax5seglem6  29028  ax5seg  29032  axpasch  29035  axeuclid  29057  uhgr2edg  29302  clwwlkccat  30085  rhmdvd  33414  bnj966  35133  bnj967  35134  mclspps  35819  cgrtr  36227  cgrtr3  36229  ofscom  36242  btwnxfr  36291  colinearxfr  36310  lineext  36311  brofs2  36312  brifs2  36313  fscgr  36315  linecgr  36316  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem5  36326  btwnconn1lem6  36327  btwnconn1lem7  36328  seglecgr12im  36345  seglecgr12  36346  segletr  36349  broutsideof3  36361  outsideofeq  36365  lineunray  36382  eqlkr  39598  omlmod1i2N  39759  cvrcmp2  39783  cvlexch2  39828  cvlexchb2  39830  cvlatexchb2  39834  cvlatexch1  39835  cvlatexch2  39836  cvlatexch3  39837  cvlsupr7  39847  cvlsupr8  39848  atnlej1  39878  atnlej2  39879  2llnneN  39908  cvratlem  39920  atcvrneN  39929  atcvrj1  39930  atlelt  39937  2atjm  39944  3noncolr2  39948  3noncolr1N  39949  hlatcon2  39951  3dimlem2  39958  3dim1  39966  3dim2  39967  1cvrat  39975  ps-1  39976  ps-2  39977  2atjlej  39978  hlatexch3N  39979  ps-2b  39981  3atlem1  39982  3atlem2  39983  3atlem6  39987  llnle  40017  2atm  40026  ps-2c  40027  lplni2  40036  lplnle  40039  lplnnle2at  40040  lplnri3N  40054  llncvrlpln2  40056  2atmat  40060  2llnjaN  40065  2llnm2N  40067  2llnm4  40069  2llnmeqat  40070  lvolnle3at  40081  4atlem0ae  40093  4atlem0be  40094  4atlem3b  40097  4atlem9  40102  4atlem10a  40103  4atlem10  40105  4atlem11a  40106  4atlem12a  40109  4at  40112  4at2  40113  lplncvrlvol2  40114  2lplnm2N  40120  2llnma1b  40285  2llnma1  40286  2llnma3r  40287  2llnma2  40288  2llnma2rN  40289  cdlema1N  40290  cdlema2N  40291  paddasslem2  40320  paddasslem15  40333  paddasslem16  40334  pmodlem1  40345  pmod2iN  40348  hlmod1i  40355  atmod2i1  40360  atmod2i2  40361  atmod3i1  40363  atmod3i2  40364  atmod4i1  40365  atmod4i2  40366  llnexchb2  40368  dalawlem3  40372  dalawlem4  40373  dalawlem5  40374  dalawlem6  40375  dalawlem7  40376  dalawlem8  40377  dalawlem9  40378  dalawlem11  40380  dalawlem13  40382  dalawlem15  40384  osumcllem7N  40461  osumcllem9N  40463  osumcllem11N  40465  pl42lem1N  40478  4atex  40575  4atex2-0aOLDN  40577  4atex2-0bOLDN  40578  4atex2-0cOLDN  40579  trlval4  40687  cdlemc5  40694  cdlemd5  40701  cdlemd6  40702  cdleme00a  40708  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme4  40737  cdleme4a  40738  cdleme16aN  40758  cdleme11c  40760  cdleme11g  40764  cdleme11h  40765  cdleme12  40770  cdleme0nex  40789  cdleme18a  40790  cdleme18b  40791  cdleme18c  40792  cdleme18d  40794  cdleme20zN  40800  cdleme20y  40801  cdleme19a  40802  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20aN  40808  cdleme20c  40810  cdleme20d  40811  cdleme20i  40816  cdleme20j  40817  cdleme20l1  40819  cdleme20l2  40820  cdleme20m  40822  cdleme21b  40825  cdleme21c  40826  cdleme21j  40835  cdleme22aa  40838  cdleme22a  40839  cdleme22eALTN  40844  cdleme26e  40858  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme27N  40868  cdleme28a  40869  cdleme28b  40870  cdleme30a  40877  cdlemefs45eN  40930  cdleme32c  40942  cdleme32e  40944  cdleme35h  40955  cdleme36a  40959  cdleme36m  40960  cdleme37m  40961  cdleme41sn3aw  40973  cdleme41sn4aw  40974  cdleme41fva11  40976  cdleme42k  40983  cdleme43cN  40990  cdleme43dN  40991  cdleme46f2g1  40993  cdlemeg47rv2  41009  cdlemeg46sfg  41019  cdlemeg46fjgN  41020  cdlemeg46rjgN  41021  cdlemeg46fjv  41022  cdlemeg46frv  41024  cdlemeg46vrg  41026  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemeg46gfv  41029  cdleme50trn2a  41049  cdlemg2fv2  41099  cdlemg4a  41107  cdlemg4e  41113  cdlemg4f  41114  cdlemg8b  41127  cdlemg8c  41128  cdlemg9a  41131  cdlemg9b  41132  cdlemg9  41133  cdlemg10a  41139  cdlemg12a  41142  cdlemg12b  41143  cdlemg12c  41144  cdlemg12  41149  cdlemg17dN  41162  cdlemg17dALTN  41163  cdlemg17e  41164  cdlemg17i  41168  cdlemg17ir  41169  cdlemg17pq  41171  cdlemg17bq  41172  cdlemg17iqN  41173  cdlemg17  41176  cdlemg18b  41178  cdlemg18c  41179  cdlemg18d  41180  cdlemg18  41181  cdlemg19  41183  cdlemg21  41185  cdlemg28a  41192  cdlemg31b0a  41194  cdlemg33b0  41200  cdlemg35  41212  cdlemg44a  41230  cdlemh  41316  cdlemi2  41318  cdlemj1  41320  cdlemk5a  41334  cdlemk5  41335  cdlemki  41340  cdlemkvcl  41341  cdlemk10  41342  cdlemksv2  41346  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemk15  41354  cdlemk16a  41355  cdlemk16  41356  cdlemk5u  41360  cdlemk6u  41361  cdlemk18  41367  cdlemk19  41368  cdlemk7u  41369  cdlemk11u  41370  cdlemk12u  41371  cdlemk21N  41372  cdlemk20  41373  cdlemkoatnle-2N  41374  cdlemk13-2N  41375  cdlemkole-2N  41376  cdlemk14-2N  41377  cdlemk15-2N  41378  cdlemk16-2N  41379  cdlemk17-2N  41380  cdlemk18-2N  41385  cdlemk19-2N  41386  cdlemk22  41392  cdlemk30  41393  cdlemk28-3  41407  cdlemk33N  41408  cdlemkfid1N  41420  cdlemkid1  41421  cdlemky  41425  cdlemk11ta  41428  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk47  41448  cdlemk48  41449  cdlemk49  41450  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  cdlemk53a  41454  cdlemk53b  41455  cdlemk53  41456  cdlemk54  41457  cdlemk55a  41458  cdlemkyyN  41461  cdlemk43N  41462  cdlemk55u1  41464  cdlemk55u  41465  cdlemk39u1  41466  cdlemk19u1  41468  cdleml1N  41475  cdleml2N  41476  cdleml3N  41477  dia2dimlem6  41568  cdlemn2  41694  cdlemn2a  41695  cdlemn5pre  41699  cdlemn11pre  41709  dihjustlem  41715  dihjust  41716  dihmeetlem15N  41820  lclkrlem2y  42030  relexpxpnnidm  44154  ormkglobd  47327  natglobalincr  47329  iscnrm3llem1  49446  iscnrm3l  49448  swapffunc  49779  fucofunc  49856