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  8523  elfiun  9357  ttrclselem2  9655  cofsmo  10198  modexp  14179  iscatd2  17618  funcoppc  17813  funcres  17834  catcisolem  18048  1stfcl  18134  2ndfcl  18135  prfcl  18140  evlfcl  18159  curf1cl  18165  curfcl  18169  hofcl  18196  pmtrprfv3  19360  mdetunilem3  22477  mdetunilem4  22478  mdetuni0  22484  mdetmul  22486  prdsxmetlem  24232  isosctrlem3  26706  isosctr  26707  noinfbnd2lem1  27618  addsass  27888  f1otrg  28774  colinearalg  28813  ax5seglem6  28837  ax5seg  28841  axpasch  28844  axeuclid  28866  uhgr2edg  29111  clwwlkccat  29892  ogrpsub  33003  ogrpsublt  33008  rhmdvd  33269  bnj966  34907  bnj967  34908  mclspps  35544  cgrtr  35953  cgrtr3  35955  ofscom  35968  btwnxfr  36017  colinearxfr  36036  lineext  36037  brofs2  36038  brifs2  36039  fscgr  36041  linecgr  36042  btwnconn1lem1  36048  btwnconn1lem2  36049  btwnconn1lem3  36050  btwnconn1lem4  36051  btwnconn1lem5  36052  btwnconn1lem6  36053  btwnconn1lem7  36054  seglecgr12im  36071  seglecgr12  36072  segletr  36075  broutsideof3  36087  outsideofeq  36091  lineunray  36108  eqlkr  39065  omlmod1i2N  39226  cvrcmp2  39250  cvlexch2  39295  cvlexchb2  39297  cvlatexchb2  39301  cvlatexch1  39302  cvlatexch2  39303  cvlatexch3  39304  cvlsupr7  39314  cvlsupr8  39315  atnlej1  39346  atnlej2  39347  2llnneN  39376  cvratlem  39388  atcvrneN  39397  atcvrj1  39398  atlelt  39405  2atjm  39412  3noncolr2  39416  3noncolr1N  39417  hlatcon2  39419  3dimlem2  39426  3dim1  39434  3dim2  39435  1cvrat  39443  ps-1  39444  ps-2  39445  2atjlej  39446  hlatexch3N  39447  ps-2b  39449  3atlem1  39450  3atlem2  39451  3atlem6  39455  llnle  39485  2atm  39494  ps-2c  39495  lplni2  39504  lplnle  39507  lplnnle2at  39508  lplnri3N  39522  llncvrlpln2  39524  2atmat  39528  2llnjaN  39533  2llnm2N  39535  2llnm4  39537  2llnmeqat  39538  lvolnle3at  39549  4atlem0ae  39561  4atlem0be  39562  4atlem3b  39565  4atlem9  39570  4atlem10a  39571  4atlem10  39573  4atlem11a  39574  4atlem12a  39577  4at  39580  4at2  39581  lplncvrlvol2  39582  2lplnm2N  39588  2llnma1b  39753  2llnma1  39754  2llnma3r  39755  2llnma2  39756  2llnma2rN  39757  cdlema1N  39758  cdlema2N  39759  paddasslem2  39788  paddasslem15  39801  paddasslem16  39802  pmodlem1  39813  pmod2iN  39816  hlmod1i  39823  atmod2i1  39828  atmod2i2  39829  atmod3i1  39831  atmod3i2  39832  atmod4i1  39833  atmod4i2  39834  llnexchb2  39836  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem13  39850  dalawlem15  39852  osumcllem7N  39929  osumcllem9N  39931  osumcllem11N  39933  pl42lem1N  39946  4atex  40043  4atex2-0aOLDN  40045  4atex2-0bOLDN  40046  4atex2-0cOLDN  40047  trlval4  40155  cdlemc5  40162  cdlemd5  40169  cdlemd6  40170  cdleme00a  40176  cdleme3g  40201  cdleme3h  40202  cdleme3  40204  cdleme4  40205  cdleme4a  40206  cdleme16aN  40226  cdleme11c  40228  cdleme11g  40232  cdleme11h  40233  cdleme12  40238  cdleme0nex  40257  cdleme18a  40258  cdleme18b  40259  cdleme18c  40260  cdleme18d  40262  cdleme20zN  40268  cdleme20y  40269  cdleme19a  40270  cdleme19b  40271  cdleme19d  40273  cdleme19e  40274  cdleme20aN  40276  cdleme20c  40278  cdleme20d  40279  cdleme20i  40284  cdleme20j  40285  cdleme20l1  40287  cdleme20l2  40288  cdleme20m  40290  cdleme21b  40293  cdleme21c  40294  cdleme21j  40303  cdleme22aa  40306  cdleme22a  40307  cdleme22eALTN  40312  cdleme26e  40326  cdleme26fALTN  40329  cdleme26f  40330  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme27N  40336  cdleme28a  40337  cdleme28b  40338  cdleme30a  40345  cdlemefs45eN  40398  cdleme32c  40410  cdleme32e  40412  cdleme35h  40423  cdleme36a  40427  cdleme36m  40428  cdleme37m  40429  cdleme41sn3aw  40441  cdleme41sn4aw  40442  cdleme41fva11  40444  cdleme42k  40451  cdleme43cN  40458  cdleme43dN  40459  cdleme46f2g1  40461  cdlemeg47rv2  40477  cdlemeg46sfg  40487  cdlemeg46fjgN  40488  cdlemeg46rjgN  40489  cdlemeg46fjv  40490  cdlemeg46frv  40492  cdlemeg46vrg  40494  cdlemeg46rgv  40495  cdlemeg46req  40496  cdlemeg46gfv  40497  cdleme50trn2a  40517  cdlemg2fv2  40567  cdlemg4a  40575  cdlemg4e  40581  cdlemg4f  40582  cdlemg8b  40595  cdlemg8c  40596  cdlemg9a  40599  cdlemg9b  40600  cdlemg9  40601  cdlemg10a  40607  cdlemg12a  40610  cdlemg12b  40611  cdlemg12c  40612  cdlemg12  40617  cdlemg17dN  40630  cdlemg17dALTN  40631  cdlemg17e  40632  cdlemg17i  40636  cdlemg17ir  40637  cdlemg17pq  40639  cdlemg17bq  40640  cdlemg17iqN  40641  cdlemg17  40644  cdlemg18b  40646  cdlemg18c  40647  cdlemg18d  40648  cdlemg18  40649  cdlemg19  40651  cdlemg21  40653  cdlemg28a  40660  cdlemg31b0a  40662  cdlemg33b0  40668  cdlemg35  40680  cdlemg44a  40698  cdlemh  40784  cdlemi2  40786  cdlemj1  40788  cdlemk5a  40802  cdlemk5  40803  cdlemki  40808  cdlemkvcl  40809  cdlemk10  40810  cdlemksv2  40814  cdlemk7  40815  cdlemk11  40816  cdlemk12  40817  cdlemk15  40822  cdlemk16a  40823  cdlemk16  40824  cdlemk5u  40828  cdlemk6u  40829  cdlemk18  40835  cdlemk19  40836  cdlemk7u  40837  cdlemk11u  40838  cdlemk12u  40839  cdlemk21N  40840  cdlemk20  40841  cdlemkoatnle-2N  40842  cdlemk13-2N  40843  cdlemkole-2N  40844  cdlemk14-2N  40845  cdlemk15-2N  40846  cdlemk16-2N  40847  cdlemk17-2N  40848  cdlemk18-2N  40853  cdlemk19-2N  40854  cdlemk22  40860  cdlemk30  40861  cdlemk28-3  40875  cdlemk33N  40876  cdlemkfid1N  40888  cdlemkid1  40889  cdlemky  40893  cdlemk11ta  40896  cdlemk35s-id  40905  cdlemk39s-id  40907  cdlemk47  40916  cdlemk48  40917  cdlemk49  40918  cdlemk50  40919  cdlemk51  40920  cdlemk52  40921  cdlemk53a  40922  cdlemk53b  40923  cdlemk53  40924  cdlemk54  40925  cdlemk55a  40926  cdlemkyyN  40929  cdlemk43N  40930  cdlemk55u1  40932  cdlemk55u  40933  cdlemk39u1  40934  cdlemk19u1  40936  cdleml1N  40943  cdleml2N  40944  cdleml3N  40945  dia2dimlem6  41036  cdlemn2  41162  cdlemn2a  41163  cdlemn5pre  41167  cdlemn11pre  41177  dihjustlem  41183  dihjust  41184  dihmeetlem15N  41288  lclkrlem2y  41498  relexpxpnnidm  43665  ormkglobd  46846  natglobalincr  46848  iscnrm3llem1  48910  iscnrm3l  48912  swapffunc  49244  fucofunc  49321