Theorem simp23 1206

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp123  1305  simp223  1314  simp323  1323  omeulem1  8375  elfiun  9119  cofsmo  9956  modexp  13881  iscatd2  17307  funcoppc  17506  funcres  17527  catcisolem  17741  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlfcl  17856  curf1cl  17862  curfcl  17866  hofcl  17893  pmtrprfv3  18977  mdetunilem3  21671  mdetunilem4  21672  mdetuni0  21678  mdetmul  21680  prdsxmetlem  23429  isosctrlem3  25875  isosctr  25876  f1otrg  27136  colinearalg  27181  ax5seglem6  27205  ax5seg  27209  axpasch  27212  axeuclid  27234  uhgr2edg  27478  clwwlkccat  28255  ogrpsub  31244  ogrpsublt  31249  rhmdvd  31422  bnj966  32824  bnj967  32825  mclspps  33446  ttrclselem2  33712  noinfbnd2lem1  33860  cgrtr  34221  cgrtr3  34223  ofscom  34236  btwnxfr  34285  colinearxfr  34304  lineext  34305  brofs2  34306  brifs2  34307  fscgr  34309  linecgr  34310  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem7  34322  seglecgr12im  34339  seglecgr12  34340  segletr  34343  broutsideof3  34355  outsideofeq  34359  lineunray  34376  eqlkr  37040  omlmod1i2N  37201  cvrcmp2  37225  cvlexch2  37270  cvlexchb2  37272  cvlatexchb2  37276  cvlatexch1  37277  cvlatexch2  37278  cvlatexch3  37279  cvlsupr7  37289  cvlsupr8  37290  atnlej1  37320  atnlej2  37321  2llnneN  37350  cvratlem  37362  atcvrneN  37371  atcvrj1  37372  atlelt  37379  2atjm  37386  3noncolr2  37390  3noncolr1N  37391  hlatcon2  37393  3dimlem2  37400  3dim1  37408  3dim2  37409  1cvrat  37417  ps-1  37418  ps-2  37419  2atjlej  37420  hlatexch3N  37421  ps-2b  37423  3atlem1  37424  3atlem2  37425  3atlem6  37429  llnle  37459  2atm  37468  ps-2c  37469  lplni2  37478  lplnle  37481  lplnnle2at  37482  lplnri3N  37496  llncvrlpln2  37498  2atmat  37502  2llnjaN  37507  2llnm2N  37509  2llnm4  37511  2llnmeqat  37512  lvolnle3at  37523  4atlem0ae  37535  4atlem0be  37536  4atlem3b  37539  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem12a  37551  4at  37554  4at2  37555  lplncvrlvol2  37556  2lplnm2N  37562  2llnma1b  37727  2llnma1  37728  2llnma3r  37729  2llnma2  37730  2llnma2rN  37731  cdlema1N  37732  cdlema2N  37733  paddasslem2  37762  paddasslem15  37775  paddasslem16  37776  pmodlem1  37787  pmod2iN  37790  hlmod1i  37797  atmod2i1  37802  atmod2i2  37803  atmod3i1  37805  atmod3i2  37806  atmod4i1  37807  atmod4i2  37808  llnexchb2  37810  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem13  37824  dalawlem15  37826  osumcllem7N  37903  osumcllem9N  37905  osumcllem11N  37907  pl42lem1N  37920  4atex  38017  4atex2-0aOLDN  38019  4atex2-0bOLDN  38020  4atex2-0cOLDN  38021  trlval4  38129  cdlemc5  38136  cdlemd5  38143  cdlemd6  38144  cdleme00a  38150  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme4a  38180  cdleme16aN  38200  cdleme11c  38202  cdleme11g  38206  cdleme11h  38207  cdleme12  38212  cdleme0nex  38231  cdleme18a  38232  cdleme18b  38233  cdleme18c  38234  cdleme18d  38236  cdleme20zN  38242  cdleme20y  38243  cdleme19a  38244  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20aN  38250  cdleme20c  38252  cdleme20d  38253  cdleme20i  38258  cdleme20j  38259  cdleme20l1  38261  cdleme20l2  38262  cdleme20m  38264  cdleme21b  38267  cdleme21c  38268  cdleme21j  38277  cdleme22aa  38280  cdleme22a  38281  cdleme22eALTN  38286  cdleme26e  38300  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme30a  38319  cdlemefs45eN  38372  cdleme32c  38384  cdleme32e  38386  cdleme35h  38397  cdleme36a  38401  cdleme36m  38402  cdleme37m  38403  cdleme41sn3aw  38415  cdleme41sn4aw  38416  cdleme41fva11  38418  cdleme42k  38425  cdleme43cN  38432  cdleme43dN  38433  cdleme46f2g1  38435  cdlemeg47rv2  38451  cdlemeg46sfg  38461  cdlemeg46fjgN  38462  cdlemeg46rjgN  38463  cdlemeg46fjv  38464  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdleme50trn2a  38491  cdlemg2fv2  38541  cdlemg4a  38549  cdlemg4e  38555  cdlemg4f  38556  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg9b  38574  cdlemg9  38575  cdlemg10a  38581  cdlemg12a  38584  cdlemg12b  38585  cdlemg12c  38586  cdlemg12  38591  cdlemg17dN  38604  cdlemg17dALTN  38605  cdlemg17e  38606  cdlemg17i  38610  cdlemg17ir  38611  cdlemg17pq  38613  cdlemg17bq  38614  cdlemg17iqN  38615  cdlemg17  38618  cdlemg18b  38620  cdlemg18c  38621  cdlemg18d  38622  cdlemg18  38623  cdlemg19  38625  cdlemg21  38627  cdlemg28a  38634  cdlemg31b0a  38636  cdlemg33b0  38642  cdlemg35  38654  cdlemg44a  38672  cdlemh  38758  cdlemi2  38760  cdlemj1  38762  cdlemk5a  38776  cdlemk5  38777  cdlemki  38782  cdlemkvcl  38783  cdlemk10  38784  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemk15  38796  cdlemk16a  38797  cdlemk16  38798  cdlemk5u  38802  cdlemk6u  38803  cdlemk18  38809  cdlemk19  38810  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk21N  38814  cdlemk20  38815  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk22  38834  cdlemk30  38835  cdlemk28-3  38849  cdlemk33N  38850  cdlemkfid1N  38862  cdlemkid1  38863  cdlemky  38867  cdlemk11ta  38870  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk47  38890  cdlemk48  38891  cdlemk49  38892  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk53a  38896  cdlemk53b  38897  cdlemk53  38898  cdlemk54  38899  cdlemk55a  38900  cdlemkyyN  38903  cdlemk43N  38904  cdlemk55u1  38906  cdlemk55u  38907  cdlemk39u1  38908  cdlemk19u1  38910  cdleml1N  38917  cdleml2N  38918  cdleml3N  38919  dia2dimlem6  39010  cdlemn2  39136  cdlemn2a  39137  cdlemn5pre  39141  cdlemn11pre  39151  dihjustlem  39157  dihjust  39158  dihmeetlem15N  39262  lclkrlem2y  39472  relexpxpnnidm  41200  iscnrm3llem1  46131  iscnrm3l  46133