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  8492  elfiun  9309  ttrclselem2  9611  cofsmo  10155  modexp  14140  iscatd2  17582  funcoppc  17777  funcres  17798  catcisolem  18012  1stfcl  18098  2ndfcl  18099  prfcl  18104  evlfcl  18123  curf1cl  18129  curfcl  18133  hofcl  18160  pmtrprfv3  19361  ogrpsub  20044  ogrpsublt  20049  mdetunilem3  22524  mdetunilem4  22525  mdetuni0  22531  mdetmul  22533  prdsxmetlem  24278  isosctrlem3  26752  isosctr  26753  noinfbnd2lem1  27664  addsass  27943  f1otrg  28844  colinearalg  28883  ax5seglem6  28907  ax5seg  28911  axpasch  28914  axeuclid  28936  uhgr2edg  29181  clwwlkccat  29962  rhmdvd  33281  bnj966  34948  bnj967  34949  mclspps  35620  cgrtr  36026  cgrtr3  36028  ofscom  36041  btwnxfr  36090  colinearxfr  36109  lineext  36110  brofs2  36111  brifs2  36112  fscgr  36114  linecgr  36115  btwnconn1lem1  36121  btwnconn1lem2  36122  btwnconn1lem3  36123  btwnconn1lem4  36124  btwnconn1lem5  36125  btwnconn1lem6  36126  btwnconn1lem7  36127  seglecgr12im  36144  seglecgr12  36145  segletr  36148  broutsideof3  36160  outsideofeq  36164  lineunray  36181  eqlkr  39138  omlmod1i2N  39299  cvrcmp2  39323  cvlexch2  39368  cvlexchb2  39370  cvlatexchb2  39374  cvlatexch1  39375  cvlatexch2  39376  cvlatexch3  39377  cvlsupr7  39387  cvlsupr8  39388  atnlej1  39418  atnlej2  39419  2llnneN  39448  cvratlem  39460  atcvrneN  39469  atcvrj1  39470  atlelt  39477  2atjm  39484  3noncolr2  39488  3noncolr1N  39489  hlatcon2  39491  3dimlem2  39498  3dim1  39506  3dim2  39507  1cvrat  39515  ps-1  39516  ps-2  39517  2atjlej  39518  hlatexch3N  39519  ps-2b  39521  3atlem1  39522  3atlem2  39523  3atlem6  39527  llnle  39557  2atm  39566  ps-2c  39567  lplni2  39576  lplnle  39579  lplnnle2at  39580  lplnri3N  39594  llncvrlpln2  39596  2atmat  39600  2llnjaN  39605  2llnm2N  39607  2llnm4  39609  2llnmeqat  39610  lvolnle3at  39621  4atlem0ae  39633  4atlem0be  39634  4atlem3b  39637  4atlem9  39642  4atlem10a  39643  4atlem10  39645  4atlem11a  39646  4atlem12a  39649  4at  39652  4at2  39653  lplncvrlvol2  39654  2lplnm2N  39660  2llnma1b  39825  2llnma1  39826  2llnma3r  39827  2llnma2  39828  2llnma2rN  39829  cdlema1N  39830  cdlema2N  39831  paddasslem2  39860  paddasslem15  39873  paddasslem16  39874  pmodlem1  39885  pmod2iN  39888  hlmod1i  39895  atmod2i1  39900  atmod2i2  39901  atmod3i1  39903  atmod3i2  39904  atmod4i1  39905  atmod4i2  39906  llnexchb2  39908  dalawlem3  39912  dalawlem4  39913  dalawlem5  39914  dalawlem6  39915  dalawlem7  39916  dalawlem8  39917  dalawlem9  39918  dalawlem11  39920  dalawlem13  39922  dalawlem15  39924  osumcllem7N  40001  osumcllem9N  40003  osumcllem11N  40005  pl42lem1N  40018  4atex  40115  4atex2-0aOLDN  40117  4atex2-0bOLDN  40118  4atex2-0cOLDN  40119  trlval4  40227  cdlemc5  40234  cdlemd5  40241  cdlemd6  40242  cdleme00a  40248  cdleme3g  40273  cdleme3h  40274  cdleme3  40276  cdleme4  40277  cdleme4a  40278  cdleme16aN  40298  cdleme11c  40300  cdleme11g  40304  cdleme11h  40305  cdleme12  40310  cdleme0nex  40329  cdleme18a  40330  cdleme18b  40331  cdleme18c  40332  cdleme18d  40334  cdleme20zN  40340  cdleme20y  40341  cdleme19a  40342  cdleme19b  40343  cdleme19d  40345  cdleme19e  40346  cdleme20aN  40348  cdleme20c  40350  cdleme20d  40351  cdleme20i  40356  cdleme20j  40357  cdleme20l1  40359  cdleme20l2  40360  cdleme20m  40362  cdleme21b  40365  cdleme21c  40366  cdleme21j  40375  cdleme22aa  40378  cdleme22a  40379  cdleme22eALTN  40384  cdleme26e  40398  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme27N  40408  cdleme28a  40409  cdleme28b  40410  cdleme30a  40417  cdlemefs45eN  40470  cdleme32c  40482  cdleme32e  40484  cdleme35h  40495  cdleme36a  40499  cdleme36m  40500  cdleme37m  40501  cdleme41sn3aw  40513  cdleme41sn4aw  40514  cdleme41fva11  40516  cdleme42k  40523  cdleme43cN  40530  cdleme43dN  40531  cdleme46f2g1  40533  cdlemeg47rv2  40549  cdlemeg46sfg  40559  cdlemeg46fjgN  40560  cdlemeg46rjgN  40561  cdlemeg46fjv  40562  cdlemeg46frv  40564  cdlemeg46vrg  40566  cdlemeg46rgv  40567  cdlemeg46req  40568  cdlemeg46gfv  40569  cdleme50trn2a  40589  cdlemg2fv2  40639  cdlemg4a  40647  cdlemg4e  40653  cdlemg4f  40654  cdlemg8b  40667  cdlemg8c  40668  cdlemg9a  40671  cdlemg9b  40672  cdlemg9  40673  cdlemg10a  40679  cdlemg12a  40682  cdlemg12b  40683  cdlemg12c  40684  cdlemg12  40689  cdlemg17dN  40702  cdlemg17dALTN  40703  cdlemg17e  40704  cdlemg17i  40708  cdlemg17ir  40709  cdlemg17pq  40711  cdlemg17bq  40712  cdlemg17iqN  40713  cdlemg17  40716  cdlemg18b  40718  cdlemg18c  40719  cdlemg18d  40720  cdlemg18  40721  cdlemg19  40723  cdlemg21  40725  cdlemg28a  40732  cdlemg31b0a  40734  cdlemg33b0  40740  cdlemg35  40752  cdlemg44a  40770  cdlemh  40856  cdlemi2  40858  cdlemj1  40860  cdlemk5a  40874  cdlemk5  40875  cdlemki  40880  cdlemkvcl  40881  cdlemk10  40882  cdlemksv2  40886  cdlemk7  40887  cdlemk11  40888  cdlemk12  40889  cdlemk15  40894  cdlemk16a  40895  cdlemk16  40896  cdlemk5u  40900  cdlemk6u  40901  cdlemk18  40907  cdlemk19  40908  cdlemk7u  40909  cdlemk11u  40910  cdlemk12u  40911  cdlemk21N  40912  cdlemk20  40913  cdlemkoatnle-2N  40914  cdlemk13-2N  40915  cdlemkole-2N  40916  cdlemk14-2N  40917  cdlemk15-2N  40918  cdlemk16-2N  40919  cdlemk17-2N  40920  cdlemk18-2N  40925  cdlemk19-2N  40926  cdlemk22  40932  cdlemk30  40933  cdlemk28-3  40947  cdlemk33N  40948  cdlemkfid1N  40960  cdlemkid1  40961  cdlemky  40965  cdlemk11ta  40968  cdlemk35s-id  40977  cdlemk39s-id  40979  cdlemk47  40988  cdlemk48  40989  cdlemk49  40990  cdlemk50  40991  cdlemk51  40992  cdlemk52  40993  cdlemk53a  40994  cdlemk53b  40995  cdlemk53  40996  cdlemk54  40997  cdlemk55a  40998  cdlemkyyN  41001  cdlemk43N  41002  cdlemk55u1  41004  cdlemk55u  41005  cdlemk39u1  41006  cdlemk19u1  41008  cdleml1N  41015  cdleml2N  41016  cdleml3N  41017  dia2dimlem6  41108  cdlemn2  41234  cdlemn2a  41235  cdlemn5pre  41239  cdlemn11pre  41249  dihjustlem  41255  dihjust  41256  dihmeetlem15N  41360  lclkrlem2y  41570  relexpxpnnidm  43736  ormkglobd  46913  natglobalincr  46915  iscnrm3llem1  48980  iscnrm3l  48982  swapffunc  49314  fucofunc  49391