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  9325  cofsmo  10171  modexp  14152  funcoppc  17790  funcres  17811  catcisolem  18025  1stfcl  18111  2ndfcl  18112  prfcl  18117  evlfcl  18136  curf1cl  18142  curfcl  18146  hofcl  18173  mulgdirlem  19026  pmtrprfv3  19374  ogrpsub  20057  ogrpaddlt  20058  ogrpsublt  20062  mdetunilem4  22550  mdetuni0  22556  mdetmul  22558  prdsxmetlem  24303  isosctrlem3  26777  isosctr  26778  amgmlem  26947  f1otrg  28869  colinearalg  28909  ax5seglem6  28933  ax5seg  28937  axpasch  28940  axeuclidlem  28961  axeuclid  28962  rhmdvd  33333  bnj966  35028  mclspps  35700  cgrtr  36108  cgrtr3  36110  ofscom  36123  cgrextend  36124  btwnxfr  36172  colinearxfr  36191  lineext  36192  fscgr  36196  linecgr  36197  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem3  36205  btwnconn1lem4  36206  btwnconn1lem5  36207  btwnconn1lem6  36208  btwnconn1lem7  36209  seglecgr12im  36226  seglecgr12  36227  segletr  36230  broutsideof3  36242  outsideofeq  36246  lineunray  36263  linecom  36266  eqlkr  39271  lshpkrlem5  39286  omlmod1i2N  39432  cvrnbtwn3  39448  cvrcmp2  39456  cvlexch2  39501  cvlexchb2  39503  cvlatexchb2  39507  cvlatexch1  39508  cvlatexch2  39509  cvlatexch3  39510  cvlsupr7  39520  cvlsupr8  39521  atnlej1  39551  atnlej2  39552  2llnneN  39581  cvratlem  39593  atcvrneN  39602  atlelt  39610  2atjm  39617  3noncolr2  39621  3noncolr1N  39622  hlatcon2  39624  3dimlem2  39631  3dim1  39639  3dim2  39640  1cvrat  39648  ps-1  39649  ps-2  39650  2atjlej  39651  hlatexch3N  39652  ps-2b  39654  3atlem1  39655  3atlem5  39659  3atlem6  39660  2atm  39699  ps-2c  39700  lplni2  39709  lplnri3N  39727  llncvrlpln2  39729  2atmat  39733  2llnm2N  39740  2llnm3N  39741  2llnm4  39742  2llnmeqat  39743  lvolnle3at  39754  4atlem0ae  39766  4atlem0be  39767  4atlem3b  39770  4atlem9  39775  4atlem10a  39776  4atlem10  39778  4atlem11a  39779  4atlem12a  39782  4at2  39786  2lplnm2N  39793  lneq2at  39950  2llnma1b  39958  2llnma1  39959  2llnma3r  39960  2llnma2  39961  2llnma2rN  39962  cdlema1N  39963  paddasslem2  39993  paddasslem16  40007  pmodlem1  40018  pmod2iN  40021  hlmod1i  40028  atmod2i1  40033  atmod2i2  40034  atmod3i1  40036  atmod3i2  40037  atmod4i1  40038  atmod4i2  40039  llnexchb2lem  40040  llnexch2N  40042  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem13  40055  dalawlem15  40057  osumcllem7N  40134  osumcllem9N  40136  pl42lem1N  40151  4atexlemswapqr  40235  4atex2  40249  4atex2-0bOLDN  40251  trlval4  40360  cdlemc5  40367  cdlemc6  40368  cdlemd2  40371  cdlemd4  40373  cdlemd6  40375  cdleme00a  40381  cdleme0e  40389  cdleme4  40410  cdleme4a  40411  cdleme5  40412  cdleme9  40425  cdleme16aN  40431  cdleme11c  40433  cdleme11dN  40434  cdleme11e  40435  cdleme11g  40437  cdleme11h  40438  cdleme11j  40439  cdleme11k  40440  cdleme11l  40441  cdleme11  40442  cdleme12  40443  cdleme13  40444  cdleme14  40445  cdleme15a  40446  cdleme15c  40448  cdleme16b  40451  cdleme16c  40452  cdleme16d  40453  cdleme16e  40454  cdleme16f  40455  cdleme17d1  40461  cdleme0nex  40462  cdleme18a  40463  cdleme18b  40464  cdleme18c  40465  cdleme18d  40467  cdlemednpq  40471  cdlemednuN  40472  cdleme20zN  40473  cdleme20y  40474  cdleme19a  40475  cdleme19b  40476  cdleme19d  40478  cdleme19e  40479  cdleme20aN  40481  cdleme20d  40484  cdleme20f  40486  cdleme20g  40487  cdleme20i  40489  cdleme20j  40490  cdleme20l1  40492  cdleme20l2  40493  cdleme20l  40494  cdleme20m  40495  cdleme21b  40498  cdleme21c  40499  cdleme21e  40503  cdleme21j  40508  cdleme22aa  40511  cdleme22a  40512  cdleme22b  40513  cdleme22cN  40514  cdleme22d  40515  cdleme22e  40516  cdleme22eALTN  40517  cdleme22f  40518  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme27N  40541  cdleme28a  40542  cdleme28b  40543  cdleme30a  40550  cdlemefs31fv1  40596  cdleme32b  40614  cdleme32c  40615  cdleme32e  40617  cdleme35h  40628  cdleme36a  40632  cdleme36m  40633  cdleme41sn3aw  40646  cdleme41sn4aw  40647  cdleme41fva11  40649  cdleme42k  40656  cdleme43cN  40663  cdleme46f2g1  40666  cdlemeg46fjgN  40693  cdlemeg46fjv  40695  cdlemeg46frv  40697  cdlemeg46rgv  40700  cdlemeg46req  40701  cdlemeg46gfv  40702  cdleme50trn2a  40722  cdlemg4a  40780  cdlemg4d  40785  cdlemg4e  40786  cdlemg4f  40787  cdlemg8c  40801  cdlemg9a  40804  cdlemg9b  40805  cdlemg10a  40812  cdlemg10  40813  cdlemg12b  40816  cdlemg12f  40820  cdlemg12g  40821  cdlemg12  40822  cdlemg17dN  40835  cdlemg17dALTN  40836  cdlemg17e  40837  cdlemg17f  40838  cdlemg17g  40839  cdlemg17i  40841  cdlemg17ir  40842  cdlemg17pq  40844  cdlemg17bq  40845  cdlemg17iqN  40846  cdlemg17  40849  cdlemg18b  40851  cdlemg18c  40852  cdlemg18d  40853  cdlemg18  40854  cdlemg19  40856  cdlemg21  40858  cdlemg28a  40865  cdlemg31b0a  40867  cdlemg27b  40868  cdlemg33b0  40873  cdlemg28b  40875  cdlemg28  40876  cdlemg35  40885  cdlemg36  40886  cdlemg44a  40903  cdlemh  40989  cdlemi2  40991  cdlemj1  40993  tendocan  40996  cdlemk5a  41007  cdlemk5  41008  cdlemki  41013  cdlemkvcl  41014  cdlemk10  41015  cdlemksv2  41019  cdlemk7  41020  cdlemk11  41021  cdlemk12  41022  cdlemkoatnle  41023  cdlemk15  41027  cdlemk16a  41028  cdlemk16  41029  cdlemk1u  41031  cdlemk5u  41033  cdlemk6u  41034  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk11u  41043  cdlemk12u  41044  cdlemk21N  41045  cdlemk20  41046  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk22  41065  cdlemk30  41066  cdlemkuel-3  41070  cdlemkuv2-3N  41071  cdlemk18-3N  41072  cdlemkfid1N  41093  cdlemkid1  41094  cdlemkfid3N  41097  cdlemky  41098  cdlemk11ta  41101  cdlemk47  41121  cdlemk48  41122  cdlemk49  41123  cdlemk50  41124  cdlemk51  41125  cdlemk52  41126  cdlemk53a  41127  cdlemk53  41129  cdlemk54  41130  cdlemk55a  41131  cdlemkyyN  41134  cdlemk43N  41135  cdlemk55u1  41137  cdlemk55u  41138  cdlemk39u1  41139  cdlemk19u1  41141  cdleml1N  41148  cdleml2N  41149  cdleml3N  41150  dia2dimlem6  41241  cdlemn2  41367  cdlemn2a  41368  cdlemn5pre  41372  cdlemn11a  41379  dihjustlem  41388  dihjust  41389  dihmeetlem15N  41493  lclkrlem2y  41703  aks6d1c1  42282  relexpmulnn  43866  ormkglobd  47035  natglobalincr  47037  iscnrm3llem1  49110  iscnrm3l  49112  swapffunc  49443  fucofunc  49520  amgmwlem  49963