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  8628  elfiun  9459  ttrclselem2  9764  cofsmo  10386  modexp  14423  iscatd2  17905  funcoppc  18100  funcres  18121  catcisolem  18335  1stfcl  18421  2ndfcl  18422  prfcl  18427  evlfcl  18446  curf1cl  18452  curfcl  18456  hofcl  18483  pmtrprfv3  19719  ogrpsub  20402  ogrpsublt  20407  mdetunilem3  22984  mdetunilem4  22985  mdetuni0  22991  mdetmul  22993  prdsxmetlem  24742  isosctrlem3  27205  isosctr  27206  noinfbnd2lem1  28144  addsass  28448  f1otrg  29505  colinearalg  29545  ax5seglem6  29569  ax5seg  29573  axpasch  29576  axeuclid  29598  uhgr2edg  29846  clwwlkccat  30638  rhmdvd  33989  bnj966  35685  bnj967  35686  mclspps  36557  cgrtr  36972  cgrtr3  36974  ofscom  36987  btwnxfr  37036  colinearxfr  37055  lineext  37056  brofs2  37057  brifs2  37058  fscgr  37060  linecgr  37061  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem3  37069  btwnconn1lem4  37070  btwnconn1lem5  37071  btwnconn1lem6  37072  btwnconn1lem7  37073  seglecgr12im  37090  seglecgr12  37091  segletr  37094  broutsideof3  37106  outsideofeq  37110  lineunray  37127  eqlkr  40422  omlmod1i2N  40583  cvrcmp2  40607  cvlexch2  40652  cvlexchb2  40654  cvlatexchb2  40658  cvlatexch1  40659  cvlatexch2  40660  cvlatexch3  40661  cvlsupr7  40671  cvlsupr8  40672  atnlej1  40702  atnlej2  40703  2llnneN  40732  cvratlem  40744  atcvrneN  40753  atcvrj1  40754  atlelt  40761  2atjm  40768  3noncolr2  40772  3noncolr1N  40773  hlatcon2  40775  3dimlem2  40782  3dim1  40790  3dim2  40791  1cvrat  40799  ps-1  40800  ps-2  40801  2atjlej  40802  hlatexch3N  40803  ps-2b  40805  3atlem1  40806  3atlem2  40807  3atlem6  40811  llnle  40841  2atm  40850  ps-2c  40851  lplni2  40860  lplnle  40863  lplnnle2at  40864  lplnri3N  40878  llncvrlpln2  40880  2atmat  40884  2llnjaN  40889  2llnm2N  40891  2llnm4  40893  2llnmeqat  40894  lvolnle3at  40905  4atlem0ae  40917  4atlem0be  40918  4atlem3b  40921  4atlem9  40926  4atlem10a  40927  4atlem10  40929  4atlem11a  40930  4atlem12a  40933  4at  40936  4at2  40937  lplncvrlvol2  40938  2lplnm2N  40944  2llnma1b  41109  2llnma1  41110  2llnma3r  41111  2llnma2  41112  2llnma2rN  41113  cdlema1N  41114  cdlema2N  41115  paddasslem2  41144  paddasslem15  41157  paddasslem16  41158  pmodlem1  41169  pmod2iN  41172  hlmod1i  41179  atmod2i1  41184  atmod2i2  41185  atmod3i1  41187  atmod3i2  41188  atmod4i1  41189  atmod4i2  41190  llnexchb2  41192  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem13  41206  dalawlem15  41208  osumcllem7N  41285  osumcllem9N  41287  osumcllem11N  41289  pl42lem1N  41302  4atex  41399  4atex2-0aOLDN  41401  4atex2-0bOLDN  41402  4atex2-0cOLDN  41403  trlval4  41511  cdlemc5  41518  cdlemd5  41525  cdlemd6  41526  cdleme00a  41532  cdleme3g  41557  cdleme3h  41558  cdleme3  41560  cdleme4  41561  cdleme4a  41562  cdleme16aN  41582  cdleme11c  41584  cdleme11g  41588  cdleme11h  41589  cdleme12  41594  cdleme0nex  41613  cdleme18a  41614  cdleme18b  41615  cdleme18c  41616  cdleme18d  41618  cdleme20zN  41624  cdleme20y  41625  cdleme19a  41626  cdleme19b  41627  cdleme19d  41629  cdleme19e  41630  cdleme20aN  41632  cdleme20c  41634  cdleme20d  41635  cdleme20i  41640  cdleme20j  41641  cdleme20l1  41643  cdleme20l2  41644  cdleme20m  41646  cdleme21b  41649  cdleme21c  41650  cdleme21j  41659  cdleme22aa  41662  cdleme22a  41663  cdleme22eALTN  41668  cdleme26e  41682  cdleme26fALTN  41685  cdleme26f  41686  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme27N  41692  cdleme28a  41693  cdleme28b  41694  cdleme30a  41701  cdlemefs45eN  41754  cdleme32c  41766  cdleme32e  41768  cdleme35h  41779  cdleme36a  41783  cdleme36m  41784  cdleme37m  41785  cdleme41sn3aw  41797  cdleme41sn4aw  41798  cdleme41fva11  41800  cdleme42k  41807  cdleme43cN  41814  cdleme43dN  41815  cdleme46f2g1  41817  cdlemeg47rv2  41833  cdlemeg46sfg  41843  cdlemeg46fjgN  41844  cdlemeg46rjgN  41845  cdlemeg46fjv  41846  cdlemeg46frv  41848  cdlemeg46vrg  41850  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemeg46gfv  41853  cdleme50trn2a  41873  cdlemg2fv2  41923  cdlemg4a  41931  cdlemg4e  41937  cdlemg4f  41938  cdlemg8b  41951  cdlemg8c  41952  cdlemg9a  41955  cdlemg9b  41956  cdlemg9  41957  cdlemg10a  41963  cdlemg12a  41966  cdlemg12b  41967  cdlemg12c  41968  cdlemg12  41973  cdlemg17dN  41986  cdlemg17dALTN  41987  cdlemg17e  41988  cdlemg17i  41992  cdlemg17ir  41993  cdlemg17pq  41995  cdlemg17bq  41996  cdlemg17iqN  41997  cdlemg17  42000  cdlemg18b  42002  cdlemg18c  42003  cdlemg18d  42004  cdlemg18  42005  cdlemg19  42007  cdlemg21  42009  cdlemg28a  42016  cdlemg31b0a  42018  cdlemg33b0  42024  cdlemg35  42036  cdlemg44a  42054  cdlemh  42140  cdlemi2  42142  cdlemj1  42144  cdlemk5a  42158  cdlemk5  42159  cdlemki  42164  cdlemkvcl  42165  cdlemk10  42166  cdlemksv2  42170  cdlemk7  42171  cdlemk11  42172  cdlemk12  42173  cdlemk15  42178  cdlemk16a  42179  cdlemk16  42180  cdlemk5u  42184  cdlemk6u  42185  cdlemk18  42191  cdlemk19  42192  cdlemk7u  42193  cdlemk11u  42194  cdlemk12u  42195  cdlemk21N  42196  cdlemk20  42197  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk22  42216  cdlemk30  42217  cdlemk28-3  42231  cdlemk33N  42232  cdlemkfid1N  42244  cdlemkid1  42245  cdlemky  42249  cdlemk11ta  42252  cdlemk35s-id  42261  cdlemk39s-id  42263  cdlemk47  42272  cdlemk48  42273  cdlemk49  42274  cdlemk50  42275  cdlemk51  42276  cdlemk52  42277  cdlemk53a  42278  cdlemk53b  42279  cdlemk53  42280  cdlemk54  42281  cdlemk55a  42282  cdlemkyyN  42285  cdlemk43N  42286  cdlemk55u1  42288  cdlemk55u  42289  cdlemk39u1  42290  cdlemk19u1  42292  cdleml1N  42299  cdleml2N  42300  cdleml3N  42301  dia2dimlem6  42392  cdlemn2  42518  cdlemn2a  42519  cdlemn5pre  42523  cdlemn11pre  42533  dihjustlem  42539  dihjust  42540  dihmeetlem15N  42644  lclkrlem2y  42854  relexpxpnnidm  44964  ormkglobd  48160  iscnrm3llem1  50394  iscnrm3l  50396  swapffunc  50735  fucofunc  50812  parmapfunc2  51105  parmapfunc  51106