Theorem simp23 1209

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8549  elfiun  9388  ttrclselem2  9686  cofsmo  10229  modexp  14210  iscatd2  17649  funcoppc  17844  funcres  17865  catcisolem  18079  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  pmtrprfv3  19391  mdetunilem3  22508  mdetunilem4  22509  mdetuni0  22515  mdetmul  22517  prdsxmetlem  24263  isosctrlem3  26737  isosctr  26738  noinfbnd2lem1  27649  addsass  27919  f1otrg  28805  colinearalg  28844  ax5seglem6  28868  ax5seg  28872  axpasch  28875  axeuclid  28897  uhgr2edg  29142  clwwlkccat  29926  ogrpsub  33037  ogrpsublt  33042  rhmdvd  33303  bnj966  34941  bnj967  34942  mclspps  35578  cgrtr  35987  cgrtr3  35989  ofscom  36002  btwnxfr  36051  colinearxfr  36070  lineext  36071  brofs2  36072  brifs2  36073  fscgr  36075  linecgr  36076  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  seglecgr12im  36105  seglecgr12  36106  segletr  36109  broutsideof3  36121  outsideofeq  36125  lineunray  36142  eqlkr  39099  omlmod1i2N  39260  cvrcmp2  39284  cvlexch2  39329  cvlexchb2  39331  cvlatexchb2  39335  cvlatexch1  39336  cvlatexch2  39337  cvlatexch3  39338  cvlsupr7  39348  cvlsupr8  39349  atnlej1  39380  atnlej2  39381  2llnneN  39410  cvratlem  39422  atcvrneN  39431  atcvrj1  39432  atlelt  39439  2atjm  39446  3noncolr2  39450  3noncolr1N  39451  hlatcon2  39453  3dimlem2  39460  3dim1  39468  3dim2  39469  1cvrat  39477  ps-1  39478  ps-2  39479  2atjlej  39480  hlatexch3N  39481  ps-2b  39483  3atlem1  39484  3atlem2  39485  3atlem6  39489  llnle  39519  2atm  39528  ps-2c  39529  lplni2  39538  lplnle  39541  lplnnle2at  39542  lplnri3N  39556  llncvrlpln2  39558  2atmat  39562  2llnjaN  39567  2llnm2N  39569  2llnm4  39571  2llnmeqat  39572  lvolnle3at  39583  4atlem0ae  39595  4atlem0be  39596  4atlem3b  39599  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem12a  39611  4at  39614  4at2  39615  lplncvrlvol2  39616  2lplnm2N  39622  2llnma1b  39787  2llnma1  39788  2llnma3r  39789  2llnma2  39790  2llnma2rN  39791  cdlema1N  39792  cdlema2N  39793  paddasslem2  39822  paddasslem15  39835  paddasslem16  39836  pmodlem1  39847  pmod2iN  39850  hlmod1i  39857  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  atmod3i2  39866  atmod4i1  39867  atmod4i2  39868  llnexchb2  39870  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem13  39884  dalawlem15  39886  osumcllem7N  39963  osumcllem9N  39965  osumcllem11N  39967  pl42lem1N  39980  4atex  40077  4atex2-0aOLDN  40079  4atex2-0bOLDN  40080  4atex2-0cOLDN  40081  trlval4  40189  cdlemc5  40196  cdlemd5  40203  cdlemd6  40204  cdleme00a  40210  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme4a  40240  cdleme16aN  40260  cdleme11c  40262  cdleme11g  40266  cdleme11h  40267  cdleme12  40272  cdleme0nex  40291  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme18d  40296  cdleme20zN  40302  cdleme20y  40303  cdleme19a  40304  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20aN  40310  cdleme20c  40312  cdleme20d  40313  cdleme20i  40318  cdleme20j  40319  cdleme20l1  40321  cdleme20l2  40322  cdleme20m  40324  cdleme21b  40327  cdleme21c  40328  cdleme21j  40337  cdleme22aa  40340  cdleme22a  40341  cdleme22eALTN  40346  cdleme26e  40360  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme30a  40379  cdlemefs45eN  40432  cdleme32c  40444  cdleme32e  40446  cdleme35h  40457  cdleme36a  40461  cdleme36m  40462  cdleme37m  40463  cdleme41sn3aw  40475  cdleme41sn4aw  40476  cdleme41fva11  40478  cdleme42k  40485  cdleme43cN  40492  cdleme43dN  40493  cdleme46f2g1  40495  cdlemeg47rv2  40511  cdlemeg46sfg  40521  cdlemeg46fjgN  40522  cdlemeg46rjgN  40523  cdlemeg46fjv  40524  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdleme50trn2a  40551  cdlemg2fv2  40601  cdlemg4a  40609  cdlemg4e  40615  cdlemg4f  40616  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg9  40635  cdlemg10a  40641  cdlemg12a  40644  cdlemg12b  40645  cdlemg12c  40646  cdlemg12  40651  cdlemg17dN  40664  cdlemg17dALTN  40665  cdlemg17e  40666  cdlemg17i  40670  cdlemg17ir  40671  cdlemg17pq  40673  cdlemg17bq  40674  cdlemg17iqN  40675  cdlemg17  40678  cdlemg18b  40680  cdlemg18c  40681  cdlemg18d  40682  cdlemg18  40683  cdlemg19  40685  cdlemg21  40687  cdlemg28a  40694  cdlemg31b0a  40696  cdlemg33b0  40702  cdlemg35  40714  cdlemg44a  40732  cdlemh  40818  cdlemi2  40820  cdlemj1  40822  cdlemk5a  40836  cdlemk5  40837  cdlemki  40842  cdlemkvcl  40843  cdlemk10  40844  cdlemksv2  40848  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemk15  40856  cdlemk16a  40857  cdlemk16  40858  cdlemk5u  40862  cdlemk6u  40863  cdlemk18  40869  cdlemk19  40870  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk21N  40874  cdlemk20  40875  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk22  40894  cdlemk30  40895  cdlemk28-3  40909  cdlemk33N  40910  cdlemkfid1N  40922  cdlemkid1  40923  cdlemky  40927  cdlemk11ta  40930  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk47  40950  cdlemk48  40951  cdlemk49  40952  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk53a  40956  cdlemk53b  40957  cdlemk53  40958  cdlemk54  40959  cdlemk55a  40960  cdlemkyyN  40963  cdlemk43N  40964  cdlemk55u1  40966  cdlemk55u  40967  cdlemk39u1  40968  cdlemk19u1  40970  cdleml1N  40977  cdleml2N  40978  cdleml3N  40979  dia2dimlem6  41070  cdlemn2  41196  cdlemn2a  41197  cdlemn5pre  41201  cdlemn11pre  41211  dihjustlem  41217  dihjust  41218  dihmeetlem15N  41322  lclkrlem2y  41532  relexpxpnnidm  43699  ormkglobd  46880  natglobalincr  46882  iscnrm3llem1  48941  iscnrm3l  48943  swapffunc  49275  fucofunc  49352