Theorem simp23 1205

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp123  1304  simp223  1313  simp323  1322  omeulem1  8191  elfiun  8878  cofsmo  9680  modexp  13595  iscatd2  16944  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  pmtrprfv3  18574  mdetunilem3  21219  mdetunilem4  21220  mdetuni0  21226  mdetmul  21228  prdsxmetlem  22975  isosctrlem3  25406  isosctr  25407  f1otrg  26665  colinearalg  26704  ax5seglem6  26728  ax5seg  26732  axpasch  26735  axeuclid  26757  uhgr2edg  26998  clwwlkccat  27775  ogrpsub  30767  ogrpsublt  30772  rhmdvd  30945  bnj966  32326  bnj967  32327  mclspps  32944  cgrtr  33566  cgrtr3  33568  ofscom  33581  btwnxfr  33630  colinearxfr  33649  lineext  33650  brofs2  33651  brifs2  33652  fscgr  33654  linecgr  33655  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem7  33667  seglecgr12im  33684  seglecgr12  33685  segletr  33688  broutsideof3  33700  outsideofeq  33704  lineunray  33721  eqlkr  36395  omlmod1i2N  36556  cvrcmp2  36580  cvlexch2  36625  cvlexchb2  36627  cvlatexchb2  36631  cvlatexch1  36632  cvlatexch2  36633  cvlatexch3  36634  cvlsupr7  36644  cvlsupr8  36645  atnlej1  36675  atnlej2  36676  2llnneN  36705  cvratlem  36717  atcvrneN  36726  atcvrj1  36727  atlelt  36734  2atjm  36741  3noncolr2  36745  3noncolr1N  36746  hlatcon2  36748  3dimlem2  36755  3dim1  36763  3dim2  36764  1cvrat  36772  ps-1  36773  ps-2  36774  2atjlej  36775  hlatexch3N  36776  ps-2b  36778  3atlem1  36779  3atlem2  36780  3atlem6  36784  llnle  36814  2atm  36823  ps-2c  36824  lplni2  36833  lplnle  36836  lplnnle2at  36837  lplnri3N  36851  llncvrlpln2  36853  2atmat  36857  2llnjaN  36862  2llnm2N  36864  2llnm4  36866  2llnmeqat  36867  lvolnle3at  36878  4atlem0ae  36890  4atlem0be  36891  4atlem3b  36894  4atlem9  36899  4atlem10a  36900  4atlem10  36902  4atlem11a  36903  4atlem12a  36906  4at  36909  4at2  36910  lplncvrlvol2  36911  2lplnm2N  36917  2llnma1b  37082  2llnma1  37083  2llnma3r  37084  2llnma2  37085  2llnma2rN  37086  cdlema1N  37087  cdlema2N  37088  paddasslem2  37117  paddasslem15  37130  paddasslem16  37131  pmodlem1  37142  pmod2iN  37145  hlmod1i  37152  atmod2i1  37157  atmod2i2  37158  atmod3i1  37160  atmod3i2  37161  atmod4i1  37162  atmod4i2  37163  llnexchb2  37165  dalawlem3  37169  dalawlem4  37170  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem9  37175  dalawlem11  37177  dalawlem13  37179  dalawlem15  37181  osumcllem7N  37258  osumcllem9N  37260  osumcllem11N  37262  pl42lem1N  37275  4atex  37372  4atex2-0aOLDN  37374  4atex2-0bOLDN  37375  4atex2-0cOLDN  37376  trlval4  37484  cdlemc5  37491  cdlemd5  37498  cdlemd6  37499  cdleme00a  37505  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme4  37534  cdleme4a  37535  cdleme16aN  37555  cdleme11c  37557  cdleme11g  37561  cdleme11h  37562  cdleme12  37567  cdleme0nex  37586  cdleme18a  37587  cdleme18b  37588  cdleme18c  37589  cdleme18d  37591  cdleme20zN  37597  cdleme20y  37598  cdleme19a  37599  cdleme19b  37600  cdleme19d  37602  cdleme19e  37603  cdleme20aN  37605  cdleme20c  37607  cdleme20d  37608  cdleme20i  37613  cdleme20j  37614  cdleme20l1  37616  cdleme20l2  37617  cdleme20m  37619  cdleme21b  37622  cdleme21c  37623  cdleme21j  37632  cdleme22aa  37635  cdleme22a  37636  cdleme22eALTN  37641  cdleme26e  37655  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme27N  37665  cdleme28a  37666  cdleme28b  37667  cdleme30a  37674  cdlemefs45eN  37727  cdleme32c  37739  cdleme32e  37741  cdleme35h  37752  cdleme36a  37756  cdleme36m  37757  cdleme37m  37758  cdleme41sn3aw  37770  cdleme41sn4aw  37771  cdleme41fva11  37773  cdleme42k  37780  cdleme43cN  37787  cdleme43dN  37788  cdleme46f2g1  37790  cdlemeg47rv2  37806  cdlemeg46sfg  37816  cdlemeg46fjgN  37817  cdlemeg46rjgN  37818  cdlemeg46fjv  37819  cdlemeg46frv  37821  cdlemeg46vrg  37823  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme50trn2a  37846  cdlemg2fv2  37896  cdlemg4a  37904  cdlemg4e  37910  cdlemg4f  37911  cdlemg8b  37924  cdlemg8c  37925  cdlemg9a  37928  cdlemg9b  37929  cdlemg9  37930  cdlemg10a  37936  cdlemg12a  37939  cdlemg12b  37940  cdlemg12c  37941  cdlemg12  37946  cdlemg17dN  37959  cdlemg17dALTN  37960  cdlemg17e  37961  cdlemg17i  37965  cdlemg17ir  37966  cdlemg17pq  37968  cdlemg17bq  37969  cdlemg17iqN  37970  cdlemg17  37973  cdlemg18b  37975  cdlemg18c  37976  cdlemg18d  37977  cdlemg18  37978  cdlemg19  37980  cdlemg21  37982  cdlemg28a  37989  cdlemg31b0a  37991  cdlemg33b0  37997  cdlemg35  38009  cdlemg44a  38027  cdlemh  38113  cdlemi2  38115  cdlemj1  38117  cdlemk5a  38131  cdlemk5  38132  cdlemki  38137  cdlemkvcl  38138  cdlemk10  38139  cdlemksv2  38143  cdlemk7  38144  cdlemk11  38145  cdlemk12  38146  cdlemk15  38151  cdlemk16a  38152  cdlemk16  38153  cdlemk5u  38157  cdlemk6u  38158  cdlemk18  38164  cdlemk19  38165  cdlemk7u  38166  cdlemk11u  38167  cdlemk12u  38168  cdlemk21N  38169  cdlemk20  38170  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk22  38189  cdlemk30  38190  cdlemk28-3  38204  cdlemk33N  38205  cdlemkfid1N  38217  cdlemkid1  38218  cdlemky  38222  cdlemk11ta  38225  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk47  38245  cdlemk48  38246  cdlemk49  38247  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  cdlemk53a  38251  cdlemk53b  38252  cdlemk53  38253  cdlemk54  38254  cdlemk55a  38255  cdlemkyyN  38258  cdlemk43N  38259  cdlemk55u1  38261  cdlemk55u  38262  cdlemk39u1  38263  cdlemk19u1  38265  cdleml1N  38272  cdleml2N  38273  cdleml3N  38274  dia2dimlem6  38365  cdlemn2  38491  cdlemn2a  38492  cdlemn5pre  38496  cdlemn11pre  38506  dihjustlem  38512  dihjust  38513  dihmeetlem15N  38617  lclkrlem2y  38827  relexpxpnnidm  40404