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 1139	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant2 1135	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8620  elfiun  9470  ttrclselem2  9766  cofsmo  10309  modexp  14277  iscatd2  17724  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  pmtrprfv3  19472  mdetunilem3  22620  mdetunilem4  22621  mdetuni0  22627  mdetmul  22629  prdsxmetlem  24378  isosctrlem3  26863  isosctr  26864  noinfbnd2lem1  27775  addsass  28038  f1otrg  28879  colinearalg  28925  ax5seglem6  28949  ax5seg  28953  axpasch  28956  axeuclid  28978  uhgr2edg  29225  clwwlkccat  30009  ogrpsub  33093  ogrpsublt  33098  rhmdvd  33348  bnj966  34958  bnj967  34959  mclspps  35589  cgrtr  35993  cgrtr3  35995  ofscom  36008  btwnxfr  36057  colinearxfr  36076  lineext  36077  brofs2  36078  brifs2  36079  fscgr  36081  linecgr  36082  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  seglecgr12im  36111  seglecgr12  36112  segletr  36115  broutsideof3  36127  outsideofeq  36131  lineunray  36148  eqlkr  39100  omlmod1i2N  39261  cvrcmp2  39285  cvlexch2  39330  cvlexchb2  39332  cvlatexchb2  39336  cvlatexch1  39337  cvlatexch2  39338  cvlatexch3  39339  cvlsupr7  39349  cvlsupr8  39350  atnlej1  39381  atnlej2  39382  2llnneN  39411  cvratlem  39423  atcvrneN  39432  atcvrj1  39433  atlelt  39440  2atjm  39447  3noncolr2  39451  3noncolr1N  39452  hlatcon2  39454  3dimlem2  39461  3dim1  39469  3dim2  39470  1cvrat  39478  ps-1  39479  ps-2  39480  2atjlej  39481  hlatexch3N  39482  ps-2b  39484  3atlem1  39485  3atlem2  39486  3atlem6  39490  llnle  39520  2atm  39529  ps-2c  39530  lplni2  39539  lplnle  39542  lplnnle2at  39543  lplnri3N  39557  llncvrlpln2  39559  2atmat  39563  2llnjaN  39568  2llnm2N  39570  2llnm4  39572  2llnmeqat  39573  lvolnle3at  39584  4atlem0ae  39596  4atlem0be  39597  4atlem3b  39600  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem12a  39612  4at  39615  4at2  39616  lplncvrlvol2  39617  2lplnm2N  39623  2llnma1b  39788  2llnma1  39789  2llnma3r  39790  2llnma2  39791  2llnma2rN  39792  cdlema1N  39793  cdlema2N  39794  paddasslem2  39823  paddasslem15  39836  paddasslem16  39837  pmodlem1  39848  pmod2iN  39851  hlmod1i  39858  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  atmod3i2  39867  atmod4i1  39868  atmod4i2  39869  llnexchb2  39871  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem13  39885  dalawlem15  39887  osumcllem7N  39964  osumcllem9N  39966  osumcllem11N  39968  pl42lem1N  39981  4atex  40078  4atex2-0aOLDN  40080  4atex2-0bOLDN  40081  4atex2-0cOLDN  40082  trlval4  40190  cdlemc5  40197  cdlemd5  40204  cdlemd6  40205  cdleme00a  40211  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme4a  40241  cdleme16aN  40261  cdleme11c  40263  cdleme11g  40267  cdleme11h  40268  cdleme12  40273  cdleme0nex  40292  cdleme18a  40293  cdleme18b  40294  cdleme18c  40295  cdleme18d  40297  cdleme20zN  40303  cdleme20y  40304  cdleme19a  40305  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20aN  40311  cdleme20c  40313  cdleme20d  40314  cdleme20i  40319  cdleme20j  40320  cdleme20l1  40322  cdleme20l2  40323  cdleme20m  40325  cdleme21b  40328  cdleme21c  40329  cdleme21j  40338  cdleme22aa  40341  cdleme22a  40342  cdleme22eALTN  40347  cdleme26e  40361  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme30a  40380  cdlemefs45eN  40433  cdleme32c  40445  cdleme32e  40447  cdleme35h  40458  cdleme36a  40462  cdleme36m  40463  cdleme37m  40464  cdleme41sn3aw  40476  cdleme41sn4aw  40477  cdleme41fva11  40479  cdleme42k  40486  cdleme43cN  40493  cdleme43dN  40494  cdleme46f2g1  40496  cdlemeg47rv2  40512  cdlemeg46sfg  40522  cdlemeg46fjgN  40523  cdlemeg46rjgN  40524  cdlemeg46fjv  40525  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdleme50trn2a  40552  cdlemg2fv2  40602  cdlemg4a  40610  cdlemg4e  40616  cdlemg4f  40617  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg9b  40635  cdlemg9  40636  cdlemg10a  40642  cdlemg12a  40645  cdlemg12b  40646  cdlemg12c  40647  cdlemg12  40652  cdlemg17dN  40665  cdlemg17dALTN  40666  cdlemg17e  40667  cdlemg17i  40671  cdlemg17ir  40672  cdlemg17pq  40674  cdlemg17bq  40675  cdlemg17iqN  40676  cdlemg17  40679  cdlemg18b  40681  cdlemg18c  40682  cdlemg18d  40683  cdlemg18  40684  cdlemg19  40686  cdlemg21  40688  cdlemg28a  40695  cdlemg31b0a  40697  cdlemg33b0  40703  cdlemg35  40715  cdlemg44a  40733  cdlemh  40819  cdlemi2  40821  cdlemj1  40823  cdlemk5a  40837  cdlemk5  40838  cdlemki  40843  cdlemkvcl  40844  cdlemk10  40845  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemk15  40857  cdlemk16a  40858  cdlemk16  40859  cdlemk5u  40863  cdlemk6u  40864  cdlemk18  40870  cdlemk19  40871  cdlemk7u  40872  cdlemk11u  40873  cdlemk12u  40874  cdlemk21N  40875  cdlemk20  40876  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk22  40895  cdlemk30  40896  cdlemk28-3  40910  cdlemk33N  40911  cdlemkfid1N  40923  cdlemkid1  40924  cdlemky  40928  cdlemk11ta  40931  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk47  40951  cdlemk48  40952  cdlemk49  40953  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk53a  40957  cdlemk53b  40958  cdlemk53  40959  cdlemk54  40960  cdlemk55a  40961  cdlemkyyN  40964  cdlemk43N  40965  cdlemk55u1  40967  cdlemk55u  40968  cdlemk39u1  40969  cdlemk19u1  40971  cdleml1N  40978  cdleml2N  40979  cdleml3N  40980  dia2dimlem6  41071  cdlemn2  41197  cdlemn2a  41198  cdlemn5pre  41202  cdlemn11pre  41212  dihjustlem  41218  dihjust  41219  dihmeetlem15N  41323  lclkrlem2y  41533  relexpxpnnidm  43716  ormkglobd  46890  natglobalincr  46892  iscnrm3llem1  48846  iscnrm3l  48848  swapffunc  48988  fucofunc  49054