Theorem simp23 1225

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  simp123  1324  simp223  1333  simp323  1342  omeulem1  8563  elfiun  9386  ttrclselem2  9691  cofsmo  10249  modexp  14270  iscatd2  17733  funcoppc  17928  funcres  17949  catcisolem  18163  1stfcl  18249  2ndfcl  18250  prfcl  18255  evlfcl  18274  curf1cl  18280  curfcl  18284  hofcl  18311  pmtrprfv3  19520  ogrpsub  20203  ogrpsublt  20208  mdetunilem3  22736  mdetunilem4  22737  mdetuni0  22743  mdetmul  22745  prdsxmetlem  24490  isosctrlem3  26947  isosctr  26948  noinfbnd2lem1  27856  addsass  28160  f1otrg  29157  colinearalg  29197  ax5seglem6  29221  ax5seg  29225  axpasch  29228  axeuclid  29250  uhgr2edg  29495  clwwlkccat  30278  rhmdvd  33583  bnj966  35273  bnj967  35274  mclspps  35971  cgrtr  36379  cgrtr3  36381  ofscom  36394  btwnxfr  36443  colinearxfr  36462  lineext  36463  brofs2  36464  brifs2  36465  fscgr  36467  linecgr  36468  btwnconn1lem1  36474  btwnconn1lem2  36475  btwnconn1lem3  36476  btwnconn1lem4  36477  btwnconn1lem5  36478  btwnconn1lem6  36479  btwnconn1lem7  36480  seglecgr12im  36497  seglecgr12  36498  segletr  36501  broutsideof3  36513  outsideofeq  36517  lineunray  36534  eqlkr  39758  omlmod1i2N  39919  cvrcmp2  39943  cvlexch2  39988  cvlexchb2  39990  cvlatexchb2  39994  cvlatexch1  39995  cvlatexch2  39996  cvlatexch3  39997  cvlsupr7  40007  cvlsupr8  40008  atnlej1  40038  atnlej2  40039  2llnneN  40068  cvratlem  40080  atcvrneN  40089  atcvrj1  40090  atlelt  40097  2atjm  40104  3noncolr2  40108  3noncolr1N  40109  hlatcon2  40111  3dimlem2  40118  3dim1  40126  3dim2  40127  1cvrat  40135  ps-1  40136  ps-2  40137  2atjlej  40138  hlatexch3N  40139  ps-2b  40141  3atlem1  40142  3atlem2  40143  3atlem6  40147  llnle  40177  2atm  40186  ps-2c  40187  lplni2  40196  lplnle  40199  lplnnle2at  40200  lplnri3N  40214  llncvrlpln2  40216  2atmat  40220  2llnjaN  40225  2llnm2N  40227  2llnm4  40229  2llnmeqat  40230  lvolnle3at  40241  4atlem0ae  40253  4atlem0be  40254  4atlem3b  40257  4atlem9  40262  4atlem10a  40263  4atlem10  40265  4atlem11a  40266  4atlem12a  40269  4at  40272  4at2  40273  lplncvrlvol2  40274  2lplnm2N  40280  2llnma1b  40445  2llnma1  40446  2llnma3r  40447  2llnma2  40448  2llnma2rN  40449  cdlema1N  40450  cdlema2N  40451  paddasslem2  40480  paddasslem15  40493  paddasslem16  40494  pmodlem1  40505  pmod2iN  40508  hlmod1i  40515  atmod2i1  40520  atmod2i2  40521  atmod3i1  40523  atmod3i2  40524  atmod4i1  40525  atmod4i2  40526  llnexchb2  40528  dalawlem3  40532  dalawlem4  40533  dalawlem5  40534  dalawlem6  40535  dalawlem7  40536  dalawlem8  40537  dalawlem9  40538  dalawlem11  40540  dalawlem13  40542  dalawlem15  40544  osumcllem7N  40621  osumcllem9N  40623  osumcllem11N  40625  pl42lem1N  40638  4atex  40735  4atex2-0aOLDN  40737  4atex2-0bOLDN  40738  4atex2-0cOLDN  40739  trlval4  40847  cdlemc5  40854  cdlemd5  40861  cdlemd6  40862  cdleme00a  40868  cdleme3g  40893  cdleme3h  40894  cdleme3  40896  cdleme4  40897  cdleme4a  40898  cdleme16aN  40918  cdleme11c  40920  cdleme11g  40924  cdleme11h  40925  cdleme12  40930  cdleme0nex  40949  cdleme18a  40950  cdleme18b  40951  cdleme18c  40952  cdleme18d  40954  cdleme20zN  40960  cdleme20y  40961  cdleme19a  40962  cdleme19b  40963  cdleme19d  40965  cdleme19e  40966  cdleme20aN  40968  cdleme20c  40970  cdleme20d  40971  cdleme20i  40976  cdleme20j  40977  cdleme20l1  40979  cdleme20l2  40980  cdleme20m  40982  cdleme21b  40985  cdleme21c  40986  cdleme21j  40995  cdleme22aa  40998  cdleme22a  40999  cdleme22eALTN  41004  cdleme26e  41018  cdleme26fALTN  41021  cdleme26f  41022  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme27N  41028  cdleme28a  41029  cdleme28b  41030  cdleme30a  41037  cdlemefs45eN  41090  cdleme32c  41102  cdleme32e  41104  cdleme35h  41115  cdleme36a  41119  cdleme36m  41120  cdleme37m  41121  cdleme41sn3aw  41133  cdleme41sn4aw  41134  cdleme41fva11  41136  cdleme42k  41143  cdleme43cN  41150  cdleme43dN  41151  cdleme46f2g1  41153  cdlemeg47rv2  41169  cdlemeg46sfg  41179  cdlemeg46fjgN  41180  cdlemeg46rjgN  41181  cdlemeg46fjv  41182  cdlemeg46frv  41184  cdlemeg46vrg  41186  cdlemeg46rgv  41187  cdlemeg46req  41188  cdlemeg46gfv  41189  cdleme50trn2a  41209  cdlemg2fv2  41259  cdlemg4a  41267  cdlemg4e  41273  cdlemg4f  41274  cdlemg8b  41287  cdlemg8c  41288  cdlemg9a  41291  cdlemg9b  41292  cdlemg9  41293  cdlemg10a  41299  cdlemg12a  41302  cdlemg12b  41303  cdlemg12c  41304  cdlemg12  41309  cdlemg17dN  41322  cdlemg17dALTN  41323  cdlemg17e  41324  cdlemg17i  41328  cdlemg17ir  41329  cdlemg17pq  41331  cdlemg17bq  41332  cdlemg17iqN  41333  cdlemg17  41336  cdlemg18b  41338  cdlemg18c  41339  cdlemg18d  41340  cdlemg18  41341  cdlemg19  41343  cdlemg21  41345  cdlemg28a  41352  cdlemg31b0a  41354  cdlemg33b0  41360  cdlemg35  41372  cdlemg44a  41390  cdlemh  41476  cdlemi2  41478  cdlemj1  41480  cdlemk5a  41494  cdlemk5  41495  cdlemki  41500  cdlemkvcl  41501  cdlemk10  41502  cdlemksv2  41506  cdlemk7  41507  cdlemk11  41508  cdlemk12  41509  cdlemk15  41514  cdlemk16a  41515  cdlemk16  41516  cdlemk5u  41520  cdlemk6u  41521  cdlemk18  41527  cdlemk19  41528  cdlemk7u  41529  cdlemk11u  41530  cdlemk12u  41531  cdlemk21N  41532  cdlemk20  41533  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk22  41552  cdlemk30  41553  cdlemk28-3  41567  cdlemk33N  41568  cdlemkfid1N  41580  cdlemkid1  41581  cdlemky  41585  cdlemk11ta  41588  cdlemk35s-id  41597  cdlemk39s-id  41599  cdlemk47  41608  cdlemk48  41609  cdlemk49  41610  cdlemk50  41611  cdlemk51  41612  cdlemk52  41613  cdlemk53a  41614  cdlemk53b  41615  cdlemk53  41616  cdlemk54  41617  cdlemk55a  41618  cdlemkyyN  41621  cdlemk43N  41622  cdlemk55u1  41624  cdlemk55u  41625  cdlemk39u1  41626  cdlemk19u1  41628  cdleml1N  41635  cdleml2N  41636  cdleml3N  41637  dia2dimlem6  41728  cdlemn2  41854  cdlemn2a  41855  cdlemn5pre  41859  cdlemn11pre  41869  dihjustlem  41875  dihjust  41876  dihmeetlem15N  41980  lclkrlem2y  42190  relexpxpnnidm  44314  ormkglobd  47476  natglobalincr  47478  iscnrm3llem1  49605  iscnrm3l  49607  swapffunc  49938  fucofunc  50015