Theorem simp22 1206

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 1136	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant2 1133	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp122  1305  simp222  1314  simp322  1323  elfiun  9198  cofsmo  10034  modexp  13962  funcoppc  17599  funcres  17620  catcisolem  17834  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlfcl  17949  curf1cl  17955  curfcl  17959  hofcl  17986  mulgdirlem  18743  pmtrprfv3  19071  mdetunilem4  21773  mdetuni0  21779  mdetmul  21781  prdsxmetlem  23530  isosctrlem3  25979  isosctr  25980  amgmlem  26148  f1otrg  27241  colinearalg  27287  ax5seglem6  27311  ax5seg  27315  axpasch  27318  axeuclidlem  27339  axeuclid  27340  ogrpsub  31351  ogrpaddlt  31352  ogrpsublt  31356  rhmdvd  31529  bnj966  32933  mclspps  33555  cgrtr  34303  cgrtr3  34305  ofscom  34318  cgrextend  34319  btwnxfr  34367  colinearxfr  34386  lineext  34387  fscgr  34391  linecgr  34392  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem7  34404  seglecgr12im  34421  seglecgr12  34422  segletr  34425  broutsideof3  34437  outsideofeq  34441  lineunray  34458  linecom  34461  eqlkr  37120  lshpkrlem5  37135  omlmod1i2N  37281  cvrnbtwn3  37297  cvrcmp2  37305  cvlexch2  37350  cvlexchb2  37352  cvlatexchb2  37356  cvlatexch1  37357  cvlatexch2  37358  cvlatexch3  37359  cvlsupr7  37369  cvlsupr8  37370  atnlej1  37400  atnlej2  37401  2llnneN  37430  cvratlem  37442  atcvrneN  37451  atlelt  37459  2atjm  37466  3noncolr2  37470  3noncolr1N  37471  hlatcon2  37473  3dimlem2  37480  3dim1  37488  3dim2  37489  1cvrat  37497  ps-1  37498  ps-2  37499  2atjlej  37500  hlatexch3N  37501  ps-2b  37503  3atlem1  37504  3atlem5  37508  3atlem6  37509  2atm  37548  ps-2c  37549  lplni2  37558  lplnri3N  37576  llncvrlpln2  37578  2atmat  37582  2llnm2N  37589  2llnm3N  37590  2llnm4  37591  2llnmeqat  37592  lvolnle3at  37603  4atlem0ae  37615  4atlem0be  37616  4atlem3b  37619  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem12a  37631  4at2  37635  2lplnm2N  37642  lneq2at  37799  2llnma1b  37807  2llnma1  37808  2llnma3r  37809  2llnma2  37810  2llnma2rN  37811  cdlema1N  37812  paddasslem2  37842  paddasslem16  37856  pmodlem1  37867  pmod2iN  37870  hlmod1i  37877  atmod2i1  37882  atmod2i2  37883  atmod3i1  37885  atmod3i2  37886  atmod4i1  37887  atmod4i2  37888  llnexchb2lem  37889  llnexch2N  37891  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem13  37904  dalawlem15  37906  osumcllem7N  37983  osumcllem9N  37985  pl42lem1N  38000  4atexlemswapqr  38084  4atex2  38098  4atex2-0bOLDN  38100  trlval4  38209  cdlemc5  38216  cdlemc6  38217  cdlemd2  38220  cdlemd4  38222  cdlemd6  38224  cdleme00a  38230  cdleme0e  38238  cdleme4  38259  cdleme4a  38260  cdleme5  38261  cdleme9  38274  cdleme16aN  38280  cdleme11c  38282  cdleme11dN  38283  cdleme11e  38284  cdleme11g  38286  cdleme11h  38287  cdleme11j  38288  cdleme11k  38289  cdleme11l  38290  cdleme11  38291  cdleme12  38292  cdleme13  38293  cdleme14  38294  cdleme15a  38295  cdleme15c  38297  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme17d1  38310  cdleme0nex  38311  cdleme18a  38312  cdleme18b  38313  cdleme18c  38314  cdleme18d  38316  cdlemednpq  38320  cdlemednuN  38321  cdleme20zN  38322  cdleme20y  38323  cdleme19a  38324  cdleme19b  38325  cdleme19d  38327  cdleme19e  38328  cdleme20aN  38330  cdleme20d  38333  cdleme20f  38335  cdleme20g  38336  cdleme20i  38338  cdleme20j  38339  cdleme20l1  38341  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21b  38347  cdleme21c  38348  cdleme21e  38352  cdleme21j  38357  cdleme22aa  38360  cdleme22a  38361  cdleme22b  38362  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme27N  38390  cdleme28a  38391  cdleme28b  38392  cdleme30a  38399  cdlemefs31fv1  38445  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35h  38477  cdleme36a  38481  cdleme36m  38482  cdleme41sn3aw  38495  cdleme41sn4aw  38496  cdleme41fva11  38498  cdleme42k  38505  cdleme43cN  38512  cdleme46f2g1  38515  cdlemeg46fjgN  38542  cdlemeg46fjv  38544  cdlemeg46frv  38546  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdleme50trn2a  38571  cdlemg4a  38629  cdlemg4d  38634  cdlemg4e  38635  cdlemg4f  38636  cdlemg8c  38650  cdlemg9a  38653  cdlemg9b  38654  cdlemg10a  38661  cdlemg10  38662  cdlemg12b  38665  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg17dN  38684  cdlemg17dALTN  38685  cdlemg17e  38686  cdlemg17f  38687  cdlemg17g  38688  cdlemg17i  38690  cdlemg17ir  38691  cdlemg17pq  38693  cdlemg17bq  38694  cdlemg17iqN  38695  cdlemg17  38698  cdlemg18b  38700  cdlemg18c  38701  cdlemg18d  38702  cdlemg18  38703  cdlemg19  38705  cdlemg21  38707  cdlemg28a  38714  cdlemg31b0a  38716  cdlemg27b  38717  cdlemg33b0  38722  cdlemg28b  38724  cdlemg28  38725  cdlemg35  38734  cdlemg36  38735  cdlemg44a  38752  cdlemh  38838  cdlemi2  38840  cdlemj1  38842  tendocan  38845  cdlemk5a  38856  cdlemk5  38857  cdlemki  38862  cdlemkvcl  38863  cdlemk10  38864  cdlemksv2  38868  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkoatnle  38872  cdlemk15  38876  cdlemk16a  38877  cdlemk16  38878  cdlemk1u  38880  cdlemk5u  38882  cdlemk6u  38883  cdlemk18  38889  cdlemk19  38890  cdlemk7u  38891  cdlemk11u  38892  cdlemk12u  38893  cdlemk21N  38894  cdlemk20  38895  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk22  38914  cdlemk30  38915  cdlemkuel-3  38919  cdlemkuv2-3N  38920  cdlemk18-3N  38921  cdlemkfid1N  38942  cdlemkid1  38943  cdlemkfid3N  38946  cdlemky  38947  cdlemk11ta  38950  cdlemk47  38970  cdlemk48  38971  cdlemk49  38972  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk53a  38976  cdlemk53  38978  cdlemk54  38979  cdlemk55a  38980  cdlemkyyN  38983  cdlemk43N  38984  cdlemk55u1  38986  cdlemk55u  38987  cdlemk39u1  38988  cdlemk19u1  38990  cdleml1N  38997  cdleml2N  38998  cdleml3N  38999  dia2dimlem6  39090  cdlemn2  39216  cdlemn2a  39217  cdlemn5pre  39221  cdlemn11a  39228  dihjustlem  39237  dihjust  39238  dihmeetlem15N  39342  lclkrlem2y  39552  relexpmulnn  41324  iscnrm3llem1  46254  iscnrm3l  46256  amgmwlem  46517  natglobalincr  46523