Theorem simp23 1210

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp123  1309  simp223  1318  simp323  1327  omeulem1  8510  elfiun  9336  ttrclselem2  9638  cofsmo  10182  modexp  14191  iscatd2  17638  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  pmtrprfv3  19420  ogrpsub  20103  ogrpsublt  20108  mdetunilem3  22589  mdetunilem4  22590  mdetuni0  22596  mdetmul  22598  prdsxmetlem  24343  isosctrlem3  26797  isosctr  26798  noinfbnd2lem1  27708  addsass  28011  f1otrg  28953  colinearalg  28993  ax5seglem6  29017  ax5seg  29021  axpasch  29024  axeuclid  29046  uhgr2edg  29291  clwwlkccat  30075  rhmdvd  33399  bnj966  35102  bnj967  35103  mclspps  35782  cgrtr  36190  cgrtr3  36192  ofscom  36205  btwnxfr  36254  colinearxfr  36273  lineext  36274  brofs2  36275  brifs2  36276  fscgr  36278  linecgr  36279  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  seglecgr12im  36308  seglecgr12  36309  segletr  36312  broutsideof3  36324  outsideofeq  36328  lineunray  36345  eqlkr  39559  omlmod1i2N  39720  cvrcmp2  39744  cvlexch2  39789  cvlexchb2  39791  cvlatexchb2  39795  cvlatexch1  39796  cvlatexch2  39797  cvlatexch3  39798  cvlsupr7  39808  cvlsupr8  39809  atnlej1  39839  atnlej2  39840  2llnneN  39869  cvratlem  39881  atcvrneN  39890  atcvrj1  39891  atlelt  39898  2atjm  39905  3noncolr2  39909  3noncolr1N  39910  hlatcon2  39912  3dimlem2  39919  3dim1  39927  3dim2  39928  1cvrat  39936  ps-1  39937  ps-2  39938  2atjlej  39939  hlatexch3N  39940  ps-2b  39942  3atlem1  39943  3atlem2  39944  3atlem6  39948  llnle  39978  2atm  39987  ps-2c  39988  lplni2  39997  lplnle  40000  lplnnle2at  40001  lplnri3N  40015  llncvrlpln2  40017  2atmat  40021  2llnjaN  40026  2llnm2N  40028  2llnm4  40030  2llnmeqat  40031  lvolnle3at  40042  4atlem0ae  40054  4atlem0be  40055  4atlem3b  40058  4atlem9  40063  4atlem10a  40064  4atlem10  40066  4atlem11a  40067  4atlem12a  40070  4at  40073  4at2  40074  lplncvrlvol2  40075  2lplnm2N  40081  2llnma1b  40246  2llnma1  40247  2llnma3r  40248  2llnma2  40249  2llnma2rN  40250  cdlema1N  40251  cdlema2N  40252  paddasslem2  40281  paddasslem15  40294  paddasslem16  40295  pmodlem1  40306  pmod2iN  40309  hlmod1i  40316  atmod2i1  40321  atmod2i2  40322  atmod3i1  40324  atmod3i2  40325  atmod4i1  40326  atmod4i2  40327  llnexchb2  40329  dalawlem3  40333  dalawlem4  40334  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem9  40339  dalawlem11  40341  dalawlem13  40343  dalawlem15  40345  osumcllem7N  40422  osumcllem9N  40424  osumcllem11N  40426  pl42lem1N  40439  4atex  40536  4atex2-0aOLDN  40538  4atex2-0bOLDN  40539  4atex2-0cOLDN  40540  trlval4  40648  cdlemc5  40655  cdlemd5  40662  cdlemd6  40663  cdleme00a  40669  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme4a  40699  cdleme16aN  40719  cdleme11c  40721  cdleme11g  40725  cdleme11h  40726  cdleme12  40731  cdleme0nex  40750  cdleme18a  40751  cdleme18b  40752  cdleme18c  40753  cdleme18d  40755  cdleme20zN  40761  cdleme20y  40762  cdleme19a  40763  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20aN  40769  cdleme20c  40771  cdleme20d  40772  cdleme20i  40777  cdleme20j  40778  cdleme20l1  40780  cdleme20l2  40781  cdleme20m  40783  cdleme21b  40786  cdleme21c  40787  cdleme21j  40796  cdleme22aa  40799  cdleme22a  40800  cdleme22eALTN  40805  cdleme26e  40819  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme30a  40838  cdlemefs45eN  40891  cdleme32c  40903  cdleme32e  40905  cdleme35h  40916  cdleme36a  40920  cdleme36m  40921  cdleme37m  40922  cdleme41sn3aw  40934  cdleme41sn4aw  40935  cdleme41fva11  40937  cdleme42k  40944  cdleme43cN  40951  cdleme43dN  40952  cdleme46f2g1  40954  cdlemeg47rv2  40970  cdlemeg46sfg  40980  cdlemeg46fjgN  40981  cdlemeg46rjgN  40982  cdlemeg46fjv  40983  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme50trn2a  41010  cdlemg2fv2  41060  cdlemg4a  41068  cdlemg4e  41074  cdlemg4f  41075  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg9  41094  cdlemg10a  41100  cdlemg12a  41103  cdlemg12b  41104  cdlemg12c  41105  cdlemg12  41110  cdlemg17dN  41123  cdlemg17dALTN  41124  cdlemg17e  41125  cdlemg17i  41129  cdlemg17ir  41130  cdlemg17pq  41132  cdlemg17bq  41133  cdlemg17iqN  41134  cdlemg17  41137  cdlemg18b  41139  cdlemg18c  41140  cdlemg18d  41141  cdlemg18  41142  cdlemg19  41144  cdlemg21  41146  cdlemg28a  41153  cdlemg31b0a  41155  cdlemg33b0  41161  cdlemg35  41173  cdlemg44a  41191  cdlemh  41277  cdlemi2  41279  cdlemj1  41281  cdlemk5a  41295  cdlemk5  41296  cdlemki  41301  cdlemkvcl  41302  cdlemk10  41303  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemk15  41315  cdlemk16a  41316  cdlemk16  41317  cdlemk5u  41321  cdlemk6u  41322  cdlemk18  41328  cdlemk19  41329  cdlemk7u  41330  cdlemk11u  41331  cdlemk12u  41332  cdlemk21N  41333  cdlemk20  41334  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk22  41353  cdlemk30  41354  cdlemk28-3  41368  cdlemk33N  41369  cdlemkfid1N  41381  cdlemkid1  41382  cdlemky  41386  cdlemk11ta  41389  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk47  41409  cdlemk48  41410  cdlemk49  41411  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdlemk53b  41416  cdlemk53  41417  cdlemk54  41418  cdlemk55a  41419  cdlemkyyN  41422  cdlemk43N  41423  cdlemk55u1  41425  cdlemk55u  41426  cdlemk39u1  41427  cdlemk19u1  41429  cdleml1N  41436  cdleml2N  41437  cdleml3N  41438  dia2dimlem6  41529  cdlemn2  41655  cdlemn2a  41656  cdlemn5pre  41660  cdlemn11pre  41670  dihjustlem  41676  dihjust  41677  dihmeetlem15N  41781  lclkrlem2y  41991  relexpxpnnidm  44148  ormkglobd  47321  natglobalincr  47323  iscnrm3llem1  49436  iscnrm3l  49438  swapffunc  49769  fucofunc  49846