Theorem simp22 1208

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp22	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simp22

Step	Hyp	Ref	Expression
1		simp2 1137	. 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:  simp122  1307  simp222  1316  simp322  1325  elfiun  9339  cofsmo  10182  modexp  14164  funcoppc  17801  funcres  17822  catcisolem  18036  1stfcl  18122  2ndfcl  18123  prfcl  18128  evlfcl  18147  curf1cl  18153  curfcl  18157  hofcl  18184  mulgdirlem  19003  pmtrprfv3  19352  ogrpsub  20035  ogrpaddlt  20036  ogrpsublt  20040  mdetunilem4  22519  mdetuni0  22525  mdetmul  22527  prdsxmetlem  24273  isosctrlem3  26747  isosctr  26748  amgmlem  26917  f1otrg  28835  colinearalg  28874  ax5seglem6  28898  ax5seg  28902  axpasch  28905  axeuclidlem  28926  axeuclid  28927  rhmdvd  33281  bnj966  34930  mclspps  35576  cgrtr  35985  cgrtr3  35987  ofscom  36000  cgrextend  36001  btwnxfr  36049  colinearxfr  36068  lineext  36069  fscgr  36073  linecgr  36074  btwnconn1lem1  36080  btwnconn1lem2  36081  btwnconn1lem3  36082  btwnconn1lem4  36083  btwnconn1lem5  36084  btwnconn1lem6  36085  btwnconn1lem7  36086  seglecgr12im  36103  seglecgr12  36104  segletr  36107  broutsideof3  36119  outsideofeq  36123  lineunray  36140  linecom  36143  eqlkr  39097  lshpkrlem5  39112  omlmod1i2N  39258  cvrnbtwn3  39274  cvrcmp2  39282  cvlexch2  39327  cvlexchb2  39329  cvlatexchb2  39333  cvlatexch1  39334  cvlatexch2  39335  cvlatexch3  39336  cvlsupr7  39346  cvlsupr8  39347  atnlej1  39378  atnlej2  39379  2llnneN  39408  cvratlem  39420  atcvrneN  39429  atlelt  39437  2atjm  39444  3noncolr2  39448  3noncolr1N  39449  hlatcon2  39451  3dimlem2  39458  3dim1  39466  3dim2  39467  1cvrat  39475  ps-1  39476  ps-2  39477  2atjlej  39478  hlatexch3N  39479  ps-2b  39481  3atlem1  39482  3atlem5  39486  3atlem6  39487  2atm  39526  ps-2c  39527  lplni2  39536  lplnri3N  39554  llncvrlpln2  39556  2atmat  39560  2llnm2N  39567  2llnm3N  39568  2llnm4  39569  2llnmeqat  39570  lvolnle3at  39581  4atlem0ae  39593  4atlem0be  39594  4atlem3b  39597  4atlem9  39602  4atlem10a  39603  4atlem10  39605  4atlem11a  39606  4atlem12a  39609  4at2  39613  2lplnm2N  39620  lneq2at  39777  2llnma1b  39785  2llnma1  39786  2llnma3r  39787  2llnma2  39788  2llnma2rN  39789  cdlema1N  39790  paddasslem2  39820  paddasslem16  39834  pmodlem1  39845  pmod2iN  39848  hlmod1i  39855  atmod2i1  39860  atmod2i2  39861  atmod3i1  39863  atmod3i2  39864  atmod4i1  39865  atmod4i2  39866  llnexchb2lem  39867  llnexch2N  39869  dalawlem3  39872  dalawlem4  39873  dalawlem5  39874  dalawlem6  39875  dalawlem7  39876  dalawlem8  39877  dalawlem9  39878  dalawlem11  39880  dalawlem12  39881  dalawlem13  39882  dalawlem15  39884  osumcllem7N  39961  osumcllem9N  39963  pl42lem1N  39978  4atexlemswapqr  40062  4atex2  40076  4atex2-0bOLDN  40078  trlval4  40187  cdlemc5  40194  cdlemc6  40195  cdlemd2  40198  cdlemd4  40200  cdlemd6  40202  cdleme00a  40208  cdleme0e  40216  cdleme4  40237  cdleme4a  40238  cdleme5  40239  cdleme9  40252  cdleme16aN  40258  cdleme11c  40260  cdleme11dN  40261  cdleme11e  40262  cdleme11g  40264  cdleme11h  40265  cdleme11j  40266  cdleme11k  40267  cdleme11l  40268  cdleme11  40269  cdleme12  40270  cdleme13  40271  cdleme14  40272  cdleme15a  40273  cdleme15c  40275  cdleme16b  40278  cdleme16c  40279  cdleme16d  40280  cdleme16e  40281  cdleme16f  40282  cdleme17d1  40288  cdleme0nex  40289  cdleme18a  40290  cdleme18b  40291  cdleme18c  40292  cdleme18d  40294  cdlemednpq  40298  cdlemednuN  40299  cdleme20zN  40300  cdleme20y  40301  cdleme19a  40302  cdleme19b  40303  cdleme19d  40305  cdleme19e  40306  cdleme20aN  40308  cdleme20d  40311  cdleme20f  40313  cdleme20g  40314  cdleme20i  40316  cdleme20j  40317  cdleme20l1  40319  cdleme20l2  40320  cdleme20l  40321  cdleme20m  40322  cdleme21b  40325  cdleme21c  40326  cdleme21e  40330  cdleme21j  40335  cdleme22aa  40338  cdleme22a  40339  cdleme22b  40340  cdleme22cN  40341  cdleme22d  40342  cdleme22e  40343  cdleme22eALTN  40344  cdleme22f  40345  cdleme26fALTN  40361  cdleme26f  40362  cdleme26f2ALTN  40363  cdleme26f2  40364  cdleme27N  40368  cdleme28a  40369  cdleme28b  40370  cdleme30a  40377  cdlemefs31fv1  40423  cdleme32b  40441  cdleme32c  40442  cdleme32e  40444  cdleme35h  40455  cdleme36a  40459  cdleme36m  40460  cdleme41sn3aw  40473  cdleme41sn4aw  40474  cdleme41fva11  40476  cdleme42k  40483  cdleme43cN  40490  cdleme46f2g1  40493  cdlemeg46fjgN  40520  cdlemeg46fjv  40522  cdlemeg46frv  40524  cdlemeg46rgv  40527  cdlemeg46req  40528  cdlemeg46gfv  40529  cdleme50trn2a  40549  cdlemg4a  40607  cdlemg4d  40612  cdlemg4e  40613  cdlemg4f  40614  cdlemg8c  40628  cdlemg9a  40631  cdlemg9b  40632  cdlemg10a  40639  cdlemg10  40640  cdlemg12b  40643  cdlemg12f  40647  cdlemg12g  40648  cdlemg12  40649  cdlemg17dN  40662  cdlemg17dALTN  40663  cdlemg17e  40664  cdlemg17f  40665  cdlemg17g  40666  cdlemg17i  40668  cdlemg17ir  40669  cdlemg17pq  40671  cdlemg17bq  40672  cdlemg17iqN  40673  cdlemg17  40676  cdlemg18b  40678  cdlemg18c  40679  cdlemg18d  40680  cdlemg18  40681  cdlemg19  40683  cdlemg21  40685  cdlemg28a  40692  cdlemg31b0a  40694  cdlemg27b  40695  cdlemg33b0  40700  cdlemg28b  40702  cdlemg28  40703  cdlemg35  40712  cdlemg36  40713  cdlemg44a  40730  cdlemh  40816  cdlemi2  40818  cdlemj1  40820  tendocan  40823  cdlemk5a  40834  cdlemk5  40835  cdlemki  40840  cdlemkvcl  40841  cdlemk10  40842  cdlemksv2  40846  cdlemk7  40847  cdlemk11  40848  cdlemk12  40849  cdlemkoatnle  40850  cdlemk15  40854  cdlemk16a  40855  cdlemk16  40856  cdlemk1u  40858  cdlemk5u  40860  cdlemk6u  40861  cdlemk18  40867  cdlemk19  40868  cdlemk7u  40869  cdlemk11u  40870  cdlemk12u  40871  cdlemk21N  40872  cdlemk20  40873  cdlemkoatnle-2N  40874  cdlemk13-2N  40875  cdlemkole-2N  40876  cdlemk14-2N  40877  cdlemk15-2N  40878  cdlemk16-2N  40879  cdlemk17-2N  40880  cdlemk18-2N  40885  cdlemk19-2N  40886  cdlemk22  40892  cdlemk30  40893  cdlemkuel-3  40897  cdlemkuv2-3N  40898  cdlemk18-3N  40899  cdlemkfid1N  40920  cdlemkid1  40921  cdlemkfid3N  40924  cdlemky  40925  cdlemk11ta  40928  cdlemk47  40948  cdlemk48  40949  cdlemk49  40950  cdlemk50  40951  cdlemk51  40952  cdlemk52  40953  cdlemk53a  40954  cdlemk53  40956  cdlemk54  40957  cdlemk55a  40958  cdlemkyyN  40961  cdlemk43N  40962  cdlemk55u1  40964  cdlemk55u  40965  cdlemk39u1  40966  cdlemk19u1  40968  cdleml1N  40975  cdleml2N  40976  cdleml3N  40977  dia2dimlem6  41068  cdlemn2  41194  cdlemn2a  41195  cdlemn5pre  41199  cdlemn11a  41206  dihjustlem  41215  dihjust  41216  dihmeetlem15N  41320  lclkrlem2y  41530  aks6d1c1  42109  relexpmulnn  43702  ormkglobd  46876  natglobalincr  46878  iscnrm3llem1  48953  iscnrm3l  48955  swapffunc  49287  fucofunc  49364  amgmwlem  49807