Theorem simp23 1227

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp123  1326  simp223  1335  simp323  1344  omeulem1  8569  elfiun  9393  ttrclselem2  9698  cofsmo  10264  modexp  14287  iscatd2  17754  funcoppc  17949  funcres  17970  catcisolem  18184  1stfcl  18270  2ndfcl  18271  prfcl  18276  evlfcl  18295  curf1cl  18301  curfcl  18305  hofcl  18332  pmtrprfv3  19547  ogrpsub  20230  ogrpsublt  20235  mdetunilem3  22800  mdetunilem4  22801  mdetuni0  22807  mdetmul  22809  prdsxmetlem  24554  isosctrlem3  27014  isosctr  27015  noinfbnd2lem1  27923  addsass  28227  f1otrg  29249  colinearalg  29289  ax5seglem6  29313  ax5seg  29317  axpasch  29320  axeuclid  29342  uhgr2edg  29587  clwwlkccat  30370  rhmdvd  33667  bnj966  35356  bnj967  35357  mclspps  36089  cgrtr  36497  cgrtr3  36499  ofscom  36512  btwnxfr  36561  colinearxfr  36580  lineext  36581  brofs2  36582  brifs2  36583  fscgr  36585  linecgr  36586  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem3  36594  btwnconn1lem4  36595  btwnconn1lem5  36596  btwnconn1lem6  36597  btwnconn1lem7  36598  seglecgr12im  36615  seglecgr12  36616  segletr  36619  broutsideof3  36631  outsideofeq  36635  lineunray  36652  eqlkr  39906  omlmod1i2N  40067  cvrcmp2  40091  cvlexch2  40136  cvlexchb2  40138  cvlatexchb2  40142  cvlatexch1  40143  cvlatexch2  40144  cvlatexch3  40145  cvlsupr7  40155  cvlsupr8  40156  atnlej1  40186  atnlej2  40187  2llnneN  40216  cvratlem  40228  atcvrneN  40237  atcvrj1  40238  atlelt  40245  2atjm  40252  3noncolr2  40256  3noncolr1N  40257  hlatcon2  40259  3dimlem2  40266  3dim1  40274  3dim2  40275  1cvrat  40283  ps-1  40284  ps-2  40285  2atjlej  40286  hlatexch3N  40287  ps-2b  40289  3atlem1  40290  3atlem2  40291  3atlem6  40295  llnle  40325  2atm  40334  ps-2c  40335  lplni2  40344  lplnle  40347  lplnnle2at  40348  lplnri3N  40362  llncvrlpln2  40364  2atmat  40368  2llnjaN  40373  2llnm2N  40375  2llnm4  40377  2llnmeqat  40378  lvolnle3at  40389  4atlem0ae  40401  4atlem0be  40402  4atlem3b  40405  4atlem9  40410  4atlem10a  40411  4atlem10  40413  4atlem11a  40414  4atlem12a  40417  4at  40420  4at2  40421  lplncvrlvol2  40422  2lplnm2N  40428  2llnma1b  40593  2llnma1  40594  2llnma3r  40595  2llnma2  40596  2llnma2rN  40597  cdlema1N  40598  cdlema2N  40599  paddasslem2  40628  paddasslem15  40641  paddasslem16  40642  pmodlem1  40653  pmod2iN  40656  hlmod1i  40663  atmod2i1  40668  atmod2i2  40669  atmod3i1  40671  atmod3i2  40672  atmod4i1  40673  atmod4i2  40674  llnexchb2  40676  dalawlem3  40680  dalawlem4  40681  dalawlem5  40682  dalawlem6  40683  dalawlem7  40684  dalawlem8  40685  dalawlem9  40686  dalawlem11  40688  dalawlem13  40690  dalawlem15  40692  osumcllem7N  40769  osumcllem9N  40771  osumcllem11N  40773  pl42lem1N  40786  4atex  40883  4atex2-0aOLDN  40885  4atex2-0bOLDN  40886  4atex2-0cOLDN  40887  trlval4  40995  cdlemc5  41002  cdlemd5  41009  cdlemd6  41010  cdleme00a  41016  cdleme3g  41041  cdleme3h  41042  cdleme3  41044  cdleme4  41045  cdleme4a  41046  cdleme16aN  41066  cdleme11c  41068  cdleme11g  41072  cdleme11h  41073  cdleme12  41078  cdleme0nex  41097  cdleme18a  41098  cdleme18b  41099  cdleme18c  41100  cdleme18d  41102  cdleme20zN  41108  cdleme20y  41109  cdleme19a  41110  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20aN  41116  cdleme20c  41118  cdleme20d  41119  cdleme20i  41124  cdleme20j  41125  cdleme20l1  41127  cdleme20l2  41128  cdleme20m  41130  cdleme21b  41133  cdleme21c  41134  cdleme21j  41143  cdleme22aa  41146  cdleme22a  41147  cdleme22eALTN  41152  cdleme26e  41166  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme27N  41176  cdleme28a  41177  cdleme28b  41178  cdleme30a  41185  cdlemefs45eN  41238  cdleme32c  41250  cdleme32e  41252  cdleme35h  41263  cdleme36a  41267  cdleme36m  41268  cdleme37m  41269  cdleme41sn3aw  41281  cdleme41sn4aw  41282  cdleme41fva11  41284  cdleme42k  41291  cdleme43cN  41298  cdleme43dN  41299  cdleme46f2g1  41301  cdlemeg47rv2  41317  cdlemeg46sfg  41327  cdlemeg46fjgN  41328  cdlemeg46rjgN  41329  cdlemeg46fjv  41330  cdlemeg46frv  41332  cdlemeg46vrg  41334  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemeg46gfv  41337  cdleme50trn2a  41357  cdlemg2fv2  41407  cdlemg4a  41415  cdlemg4e  41421  cdlemg4f  41422  cdlemg8b  41435  cdlemg8c  41436  cdlemg9a  41439  cdlemg9b  41440  cdlemg9  41441  cdlemg10a  41447  cdlemg12a  41450  cdlemg12b  41451  cdlemg12c  41452  cdlemg12  41457  cdlemg17dN  41470  cdlemg17dALTN  41471  cdlemg17e  41472  cdlemg17i  41476  cdlemg17ir  41477  cdlemg17pq  41479  cdlemg17bq  41480  cdlemg17iqN  41481  cdlemg17  41484  cdlemg18b  41486  cdlemg18c  41487  cdlemg18d  41488  cdlemg18  41489  cdlemg19  41491  cdlemg21  41493  cdlemg28a  41500  cdlemg31b0a  41502  cdlemg33b0  41508  cdlemg35  41520  cdlemg44a  41538  cdlemh  41624  cdlemi2  41626  cdlemj1  41628  cdlemk5a  41642  cdlemk5  41643  cdlemki  41648  cdlemkvcl  41649  cdlemk10  41650  cdlemksv2  41654  cdlemk7  41655  cdlemk11  41656  cdlemk12  41657  cdlemk15  41662  cdlemk16a  41663  cdlemk16  41664  cdlemk5u  41668  cdlemk6u  41669  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk11u  41678  cdlemk12u  41679  cdlemk21N  41680  cdlemk20  41681  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk22  41700  cdlemk30  41701  cdlemk28-3  41715  cdlemk33N  41716  cdlemkfid1N  41728  cdlemkid1  41729  cdlemky  41733  cdlemk11ta  41736  cdlemk35s-id  41745  cdlemk39s-id  41747  cdlemk47  41756  cdlemk48  41757  cdlemk49  41758  cdlemk50  41759  cdlemk51  41760  cdlemk52  41761  cdlemk53a  41762  cdlemk53b  41763  cdlemk53  41764  cdlemk54  41765  cdlemk55a  41766  cdlemkyyN  41769  cdlemk43N  41770  cdlemk55u1  41772  cdlemk55u  41773  cdlemk39u1  41774  cdlemk19u1  41776  cdleml1N  41783  cdleml2N  41784  cdleml3N  41785  dia2dimlem6  41876  cdlemn2  42002  cdlemn2a  42003  cdlemn5pre  42007  cdlemn11pre  42017  dihjustlem  42023  dihjust  42024  dihmeetlem15N  42128  lclkrlem2y  42338  relexpxpnnidm  44462  ormkglobd  47624  natglobalincr  47626  iscnrm3llem1  49760  iscnrm3l  49762  swapffunc  50093  fucofunc  50170