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  8511  elfiun  9337  ttrclselem2  9639  cofsmo  10183  modexp  14165  iscatd2  17608  funcoppc  17803  funcres  17824  catcisolem  18038  1stfcl  18124  2ndfcl  18125  prfcl  18130  evlfcl  18149  curf1cl  18155  curfcl  18159  hofcl  18186  pmtrprfv3  19387  ogrpsub  20070  ogrpsublt  20075  mdetunilem3  22562  mdetunilem4  22563  mdetuni0  22569  mdetmul  22571  prdsxmetlem  24316  isosctrlem3  26790  isosctr  26791  noinfbnd2lem1  27702  addsass  27987  f1otrg  28926  colinearalg  28966  ax5seglem6  28990  ax5seg  28994  axpasch  28997  axeuclid  29019  uhgr2edg  29264  clwwlkccat  30048  rhmdvd  33386  bnj966  35081  bnj967  35082  mclspps  35759  cgrtr  36167  cgrtr3  36169  ofscom  36182  btwnxfr  36231  colinearxfr  36250  lineext  36251  brofs2  36252  brifs2  36253  fscgr  36255  linecgr  36256  btwnconn1lem1  36262  btwnconn1lem2  36263  btwnconn1lem3  36264  btwnconn1lem4  36265  btwnconn1lem5  36266  btwnconn1lem6  36267  btwnconn1lem7  36268  seglecgr12im  36285  seglecgr12  36286  segletr  36289  broutsideof3  36301  outsideofeq  36305  lineunray  36322  eqlkr  39396  omlmod1i2N  39557  cvrcmp2  39581  cvlexch2  39626  cvlexchb2  39628  cvlatexchb2  39632  cvlatexch1  39633  cvlatexch2  39634  cvlatexch3  39635  cvlsupr7  39645  cvlsupr8  39646  atnlej1  39676  atnlej2  39677  2llnneN  39706  cvratlem  39718  atcvrneN  39727  atcvrj1  39728  atlelt  39735  2atjm  39742  3noncolr2  39746  3noncolr1N  39747  hlatcon2  39749  3dimlem2  39756  3dim1  39764  3dim2  39765  1cvrat  39773  ps-1  39774  ps-2  39775  2atjlej  39776  hlatexch3N  39777  ps-2b  39779  3atlem1  39780  3atlem2  39781  3atlem6  39785  llnle  39815  2atm  39824  ps-2c  39825  lplni2  39834  lplnle  39837  lplnnle2at  39838  lplnri3N  39852  llncvrlpln2  39854  2atmat  39858  2llnjaN  39863  2llnm2N  39865  2llnm4  39867  2llnmeqat  39868  lvolnle3at  39879  4atlem0ae  39891  4atlem0be  39892  4atlem3b  39895  4atlem9  39900  4atlem10a  39901  4atlem10  39903  4atlem11a  39904  4atlem12a  39907  4at  39910  4at2  39911  lplncvrlvol2  39912  2lplnm2N  39918  2llnma1b  40083  2llnma1  40084  2llnma3r  40085  2llnma2  40086  2llnma2rN  40087  cdlema1N  40088  cdlema2N  40089  paddasslem2  40118  paddasslem15  40131  paddasslem16  40132  pmodlem1  40143  pmod2iN  40146  hlmod1i  40153  atmod2i1  40158  atmod2i2  40159  atmod3i1  40161  atmod3i2  40162  atmod4i1  40163  atmod4i2  40164  llnexchb2  40166  dalawlem3  40170  dalawlem4  40171  dalawlem5  40172  dalawlem6  40173  dalawlem7  40174  dalawlem8  40175  dalawlem9  40176  dalawlem11  40178  dalawlem13  40180  dalawlem15  40182  osumcllem7N  40259  osumcllem9N  40261  osumcllem11N  40263  pl42lem1N  40276  4atex  40373  4atex2-0aOLDN  40375  4atex2-0bOLDN  40376  4atex2-0cOLDN  40377  trlval4  40485  cdlemc5  40492  cdlemd5  40499  cdlemd6  40500  cdleme00a  40506  cdleme3g  40531  cdleme3h  40532  cdleme3  40534  cdleme4  40535  cdleme4a  40536  cdleme16aN  40556  cdleme11c  40558  cdleme11g  40562  cdleme11h  40563  cdleme12  40568  cdleme0nex  40587  cdleme18a  40588  cdleme18b  40589  cdleme18c  40590  cdleme18d  40592  cdleme20zN  40598  cdleme20y  40599  cdleme19a  40600  cdleme19b  40601  cdleme19d  40603  cdleme19e  40604  cdleme20aN  40606  cdleme20c  40608  cdleme20d  40609  cdleme20i  40614  cdleme20j  40615  cdleme20l1  40617  cdleme20l2  40618  cdleme20m  40620  cdleme21b  40623  cdleme21c  40624  cdleme21j  40633  cdleme22aa  40636  cdleme22a  40637  cdleme22eALTN  40642  cdleme26e  40656  cdleme26fALTN  40659  cdleme26f  40660  cdleme26f2ALTN  40661  cdleme26f2  40662  cdleme27N  40666  cdleme28a  40667  cdleme28b  40668  cdleme30a  40675  cdlemefs45eN  40728  cdleme32c  40740  cdleme32e  40742  cdleme35h  40753  cdleme36a  40757  cdleme36m  40758  cdleme37m  40759  cdleme41sn3aw  40771  cdleme41sn4aw  40772  cdleme41fva11  40774  cdleme42k  40781  cdleme43cN  40788  cdleme43dN  40789  cdleme46f2g1  40791  cdlemeg47rv2  40807  cdlemeg46sfg  40817  cdlemeg46fjgN  40818  cdlemeg46rjgN  40819  cdlemeg46fjv  40820  cdlemeg46frv  40822  cdlemeg46vrg  40824  cdlemeg46rgv  40825  cdlemeg46req  40826  cdlemeg46gfv  40827  cdleme50trn2a  40847  cdlemg2fv2  40897  cdlemg4a  40905  cdlemg4e  40911  cdlemg4f  40912  cdlemg8b  40925  cdlemg8c  40926  cdlemg9a  40929  cdlemg9b  40930  cdlemg9  40931  cdlemg10a  40937  cdlemg12a  40940  cdlemg12b  40941  cdlemg12c  40942  cdlemg12  40947  cdlemg17dN  40960  cdlemg17dALTN  40961  cdlemg17e  40962  cdlemg17i  40966  cdlemg17ir  40967  cdlemg17pq  40969  cdlemg17bq  40970  cdlemg17iqN  40971  cdlemg17  40974  cdlemg18b  40976  cdlemg18c  40977  cdlemg18d  40978  cdlemg18  40979  cdlemg19  40981  cdlemg21  40983  cdlemg28a  40990  cdlemg31b0a  40992  cdlemg33b0  40998  cdlemg35  41010  cdlemg44a  41028  cdlemh  41114  cdlemi2  41116  cdlemj1  41118  cdlemk5a  41132  cdlemk5  41133  cdlemki  41138  cdlemkvcl  41139  cdlemk10  41140  cdlemksv2  41144  cdlemk7  41145  cdlemk11  41146  cdlemk12  41147  cdlemk15  41152  cdlemk16a  41153  cdlemk16  41154  cdlemk5u  41158  cdlemk6u  41159  cdlemk18  41165  cdlemk19  41166  cdlemk7u  41167  cdlemk11u  41168  cdlemk12u  41169  cdlemk21N  41170  cdlemk20  41171  cdlemkoatnle-2N  41172  cdlemk13-2N  41173  cdlemkole-2N  41174  cdlemk14-2N  41175  cdlemk15-2N  41176  cdlemk16-2N  41177  cdlemk17-2N  41178  cdlemk18-2N  41183  cdlemk19-2N  41184  cdlemk22  41190  cdlemk30  41191  cdlemk28-3  41205  cdlemk33N  41206  cdlemkfid1N  41218  cdlemkid1  41219  cdlemky  41223  cdlemk11ta  41226  cdlemk35s-id  41235  cdlemk39s-id  41237  cdlemk47  41246  cdlemk48  41247  cdlemk49  41248  cdlemk50  41249  cdlemk51  41250  cdlemk52  41251  cdlemk53a  41252  cdlemk53b  41253  cdlemk53  41254  cdlemk54  41255  cdlemk55a  41256  cdlemkyyN  41259  cdlemk43N  41260  cdlemk55u1  41262  cdlemk55u  41263  cdlemk39u1  41264  cdlemk19u1  41266  cdleml1N  41273  cdleml2N  41274  cdleml3N  41275  dia2dimlem6  41366  cdlemn2  41492  cdlemn2a  41493  cdlemn5pre  41497  cdlemn11pre  41507  dihjustlem  41513  dihjust  41514  dihmeetlem15N  41618  lclkrlem2y  41828  relexpxpnnidm  43980  ormkglobd  47155  natglobalincr  47157  iscnrm3llem1  49230  iscnrm3l  49232  swapffunc  49563  fucofunc  49640