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  8583  elfiun  9415  ttrclselem2  9720  cofsmo  10340  modexp  14375  iscatd2  17848  funcoppc  18043  funcres  18064  catcisolem  18278  1stfcl  18364  2ndfcl  18365  prfcl  18370  evlfcl  18389  curf1cl  18395  curfcl  18399  hofcl  18426  pmtrprfv3  19661  ogrpsub  20344  ogrpsublt  20349  mdetunilem3  22922  mdetunilem4  22923  mdetuni0  22929  mdetmul  22931  prdsxmetlem  24680  isosctrlem3  27141  isosctr  27142  noinfbnd2lem1  28080  addsass  28384  f1otrg  29441  colinearalg  29481  ax5seglem6  29505  ax5seg  29509  axpasch  29512  axeuclid  29534  uhgr2edg  29782  clwwlkccat  30574  rhmdvd  33878  bnj966  35567  bnj967  35568  mclspps  36328  cgrtr  36737  cgrtr3  36739  ofscom  36752  btwnxfr  36801  colinearxfr  36820  lineext  36821  brofs2  36822  brifs2  36823  fscgr  36825  linecgr  36826  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem3  36834  btwnconn1lem4  36835  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem7  36838  seglecgr12im  36855  seglecgr12  36856  segletr  36859  broutsideof3  36871  outsideofeq  36875  lineunray  36892  eqlkr  40136  omlmod1i2N  40297  cvrcmp2  40321  cvlexch2  40366  cvlexchb2  40368  cvlatexchb2  40372  cvlatexch1  40373  cvlatexch2  40374  cvlatexch3  40375  cvlsupr7  40385  cvlsupr8  40386  atnlej1  40416  atnlej2  40417  2llnneN  40446  cvratlem  40458  atcvrneN  40467  atcvrj1  40468  atlelt  40475  2atjm  40482  3noncolr2  40486  3noncolr1N  40487  hlatcon2  40489  3dimlem2  40496  3dim1  40504  3dim2  40505  1cvrat  40513  ps-1  40514  ps-2  40515  2atjlej  40516  hlatexch3N  40517  ps-2b  40519  3atlem1  40520  3atlem2  40521  3atlem6  40525  llnle  40555  2atm  40564  ps-2c  40565  lplni2  40574  lplnle  40577  lplnnle2at  40578  lplnri3N  40592  llncvrlpln2  40594  2atmat  40598  2llnjaN  40603  2llnm2N  40605  2llnm4  40607  2llnmeqat  40608  lvolnle3at  40619  4atlem0ae  40631  4atlem0be  40632  4atlem3b  40635  4atlem9  40640  4atlem10a  40641  4atlem10  40643  4atlem11a  40644  4atlem12a  40647  4at  40650  4at2  40651  lplncvrlvol2  40652  2lplnm2N  40658  2llnma1b  40823  2llnma1  40824  2llnma3r  40825  2llnma2  40826  2llnma2rN  40827  cdlema1N  40828  cdlema2N  40829  paddasslem2  40858  paddasslem15  40871  paddasslem16  40872  pmodlem1  40883  pmod2iN  40886  hlmod1i  40893  atmod2i1  40898  atmod2i2  40899  atmod3i1  40901  atmod3i2  40902  atmod4i1  40903  atmod4i2  40904  llnexchb2  40906  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem13  40920  dalawlem15  40922  osumcllem7N  40999  osumcllem9N  41001  osumcllem11N  41003  pl42lem1N  41016  4atex  41113  4atex2-0aOLDN  41115  4atex2-0bOLDN  41116  4atex2-0cOLDN  41117  trlval4  41225  cdlemc5  41232  cdlemd5  41239  cdlemd6  41240  cdleme00a  41246  cdleme3g  41271  cdleme3h  41272  cdleme3  41274  cdleme4  41275  cdleme4a  41276  cdleme16aN  41296  cdleme11c  41298  cdleme11g  41302  cdleme11h  41303  cdleme12  41308  cdleme0nex  41327  cdleme18a  41328  cdleme18b  41329  cdleme18c  41330  cdleme18d  41332  cdleme20zN  41338  cdleme20y  41339  cdleme19a  41340  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20aN  41346  cdleme20c  41348  cdleme20d  41349  cdleme20i  41354  cdleme20j  41355  cdleme20l1  41357  cdleme20l2  41358  cdleme20m  41360  cdleme21b  41363  cdleme21c  41364  cdleme21j  41373  cdleme22aa  41376  cdleme22a  41377  cdleme22eALTN  41382  cdleme26e  41396  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme27N  41406  cdleme28a  41407  cdleme28b  41408  cdleme30a  41415  cdlemefs45eN  41468  cdleme32c  41480  cdleme32e  41482  cdleme35h  41493  cdleme36a  41497  cdleme36m  41498  cdleme37m  41499  cdleme41sn3aw  41511  cdleme41sn4aw  41512  cdleme41fva11  41514  cdleme42k  41521  cdleme43cN  41528  cdleme43dN  41529  cdleme46f2g1  41531  cdlemeg47rv2  41547  cdlemeg46sfg  41557  cdlemeg46fjgN  41558  cdlemeg46rjgN  41559  cdlemeg46fjv  41560  cdlemeg46frv  41562  cdlemeg46vrg  41564  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemeg46gfv  41567  cdleme50trn2a  41587  cdlemg2fv2  41637  cdlemg4a  41645  cdlemg4e  41651  cdlemg4f  41652  cdlemg8b  41665  cdlemg8c  41666  cdlemg9a  41669  cdlemg9b  41670  cdlemg9  41671  cdlemg10a  41677  cdlemg12a  41680  cdlemg12b  41681  cdlemg12c  41682  cdlemg12  41687  cdlemg17dN  41700  cdlemg17dALTN  41701  cdlemg17e  41702  cdlemg17i  41706  cdlemg17ir  41707  cdlemg17pq  41709  cdlemg17bq  41710  cdlemg17iqN  41711  cdlemg17  41714  cdlemg18b  41716  cdlemg18c  41717  cdlemg18d  41718  cdlemg18  41719  cdlemg19  41721  cdlemg21  41723  cdlemg28a  41730  cdlemg31b0a  41732  cdlemg33b0  41738  cdlemg35  41750  cdlemg44a  41768  cdlemh  41854  cdlemi2  41856  cdlemj1  41858  cdlemk5a  41872  cdlemk5  41873  cdlemki  41878  cdlemkvcl  41879  cdlemk10  41880  cdlemksv2  41884  cdlemk7  41885  cdlemk11  41886  cdlemk12  41887  cdlemk15  41892  cdlemk16a  41893  cdlemk16  41894  cdlemk5u  41898  cdlemk6u  41899  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk11u  41908  cdlemk12u  41909  cdlemk21N  41910  cdlemk20  41911  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk22  41930  cdlemk30  41931  cdlemk28-3  41945  cdlemk33N  41946  cdlemkfid1N  41958  cdlemkid1  41959  cdlemky  41963  cdlemk11ta  41966  cdlemk35s-id  41975  cdlemk39s-id  41977  cdlemk47  41986  cdlemk48  41987  cdlemk49  41988  cdlemk50  41989  cdlemk51  41990  cdlemk52  41991  cdlemk53a  41992  cdlemk53b  41993  cdlemk53  41994  cdlemk54  41995  cdlemk55a  41996  cdlemkyyN  41999  cdlemk43N  42000  cdlemk55u1  42002  cdlemk55u  42003  cdlemk39u1  42004  cdlemk19u1  42006  cdleml1N  42013  cdleml2N  42014  cdleml3N  42015  dia2dimlem6  42106  cdlemn2  42232  cdlemn2a  42233  cdlemn5pre  42237  cdlemn11pre  42247  dihjustlem  42253  dihjust  42254  dihmeetlem15N  42358  lclkrlem2y  42568  relexpxpnnidm  44688  ormkglobd  47856  iscnrm3llem1  50026  iscnrm3l  50028  swapffunc  50359  fucofunc  50436