Theorem simp22 1217

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 1146	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant2 1143	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  simp122  1316  simp222  1325  simp322  1334  elfiun  9362  cofsmo  10212  modexp  14237  funcoppc  17880  funcres  17901  catcisolem  18115  1stfcl  18201  2ndfcl  18202  prfcl  18207  evlfcl  18226  curf1cl  18232  curfcl  18236  hofcl  18263  mulgdirlem  19119  pmtrprfv3  19466  ogrpsub  20149  ogrpaddlt  20150  ogrpsublt  20154  mdetunilem4  22644  mdetuni0  22650  mdetmul  22652  prdsxmetlem  24397  isosctrlem3  26851  isosctr  26852  amgmlem  27020  f1otrg  29006  colinearalg  29046  ax5seglem6  29070  ax5seg  29074  axpasch  29077  axeuclidlem  29098  axeuclid  29099  rhmdvd  33456  bnj966  35186  mclspps  35872  cgrtr  36280  cgrtr3  36282  ofscom  36295  cgrextend  36296  btwnxfr  36344  colinearxfr  36363  lineext  36364  fscgr  36368  linecgr  36369  btwnconn1lem1  36375  btwnconn1lem2  36376  btwnconn1lem3  36377  btwnconn1lem4  36378  btwnconn1lem5  36379  btwnconn1lem6  36380  btwnconn1lem7  36381  seglecgr12im  36398  seglecgr12  36399  segletr  36402  broutsideof3  36414  outsideofeq  36418  lineunray  36435  linecom  36438  eqlkr  39661  lshpkrlem5  39676  omlmod1i2N  39822  cvrnbtwn3  39838  cvrcmp2  39846  cvlexch2  39891  cvlexchb2  39893  cvlatexchb2  39897  cvlatexch1  39898  cvlatexch2  39899  cvlatexch3  39900  cvlsupr7  39910  cvlsupr8  39911  atnlej1  39941  atnlej2  39942  2llnneN  39971  cvratlem  39983  atcvrneN  39992  atlelt  40000  2atjm  40007  3noncolr2  40011  3noncolr1N  40012  hlatcon2  40014  3dimlem2  40021  3dim1  40029  3dim2  40030  1cvrat  40038  ps-1  40039  ps-2  40040  2atjlej  40041  hlatexch3N  40042  ps-2b  40044  3atlem1  40045  3atlem5  40049  3atlem6  40050  2atm  40089  ps-2c  40090  lplni2  40099  lplnri3N  40117  llncvrlpln2  40119  2atmat  40123  2llnm2N  40130  2llnm3N  40131  2llnm4  40132  2llnmeqat  40133  lvolnle3at  40144  4atlem0ae  40156  4atlem0be  40157  4atlem3b  40160  4atlem9  40165  4atlem10a  40166  4atlem10  40168  4atlem11a  40169  4atlem12a  40172  4at2  40176  2lplnm2N  40183  lneq2at  40340  2llnma1b  40348  2llnma1  40349  2llnma3r  40350  2llnma2  40351  2llnma2rN  40352  cdlema1N  40353  paddasslem2  40383  paddasslem16  40397  pmodlem1  40408  pmod2iN  40411  hlmod1i  40418  atmod2i1  40423  atmod2i2  40424  atmod3i1  40426  atmod3i2  40427  atmod4i1  40428  atmod4i2  40429  llnexchb2lem  40430  llnexch2N  40432  dalawlem3  40435  dalawlem4  40436  dalawlem5  40437  dalawlem6  40438  dalawlem7  40439  dalawlem8  40440  dalawlem9  40441  dalawlem11  40443  dalawlem12  40444  dalawlem13  40445  dalawlem15  40447  osumcllem7N  40524  osumcllem9N  40526  pl42lem1N  40541  4atexlemswapqr  40625  4atex2  40639  4atex2-0bOLDN  40641  trlval4  40750  cdlemc5  40757  cdlemc6  40758  cdlemd2  40761  cdlemd4  40763  cdlemd6  40765  cdleme00a  40771  cdleme0e  40779  cdleme4  40800  cdleme4a  40801  cdleme5  40802  cdleme9  40815  cdleme16aN  40821  cdleme11c  40823  cdleme11dN  40824  cdleme11e  40825  cdleme11g  40827  cdleme11h  40828  cdleme11j  40829  cdleme11k  40830  cdleme11l  40831  cdleme11  40832  cdleme12  40833  cdleme13  40834  cdleme14  40835  cdleme15a  40836  cdleme15c  40838  cdleme16b  40841  cdleme16c  40842  cdleme16d  40843  cdleme16e  40844  cdleme16f  40845  cdleme17d1  40851  cdleme0nex  40852  cdleme18a  40853  cdleme18b  40854  cdleme18c  40855  cdleme18d  40857  cdlemednpq  40861  cdlemednuN  40862  cdleme20zN  40863  cdleme20y  40864  cdleme19a  40865  cdleme19b  40866  cdleme19d  40868  cdleme19e  40869  cdleme20aN  40871  cdleme20d  40874  cdleme20f  40876  cdleme20g  40877  cdleme20i  40879  cdleme20j  40880  cdleme20l1  40882  cdleme20l2  40883  cdleme20l  40884  cdleme20m  40885  cdleme21b  40888  cdleme21c  40889  cdleme21e  40893  cdleme21j  40898  cdleme22aa  40901  cdleme22a  40902  cdleme22b  40903  cdleme22cN  40904  cdleme22d  40905  cdleme22e  40906  cdleme22eALTN  40907  cdleme22f  40908  cdleme26fALTN  40924  cdleme26f  40925  cdleme26f2ALTN  40926  cdleme26f2  40927  cdleme27N  40931  cdleme28a  40932  cdleme28b  40933  cdleme30a  40940  cdlemefs31fv1  40986  cdleme32b  41004  cdleme32c  41005  cdleme32e  41007  cdleme35h  41018  cdleme36a  41022  cdleme36m  41023  cdleme41sn3aw  41036  cdleme41sn4aw  41037  cdleme41fva11  41039  cdleme42k  41046  cdleme43cN  41053  cdleme46f2g1  41056  cdlemeg46fjgN  41083  cdlemeg46fjv  41085  cdlemeg46frv  41087  cdlemeg46rgv  41090  cdlemeg46req  41091  cdlemeg46gfv  41092  cdleme50trn2a  41112  cdlemg4a  41170  cdlemg4d  41175  cdlemg4e  41176  cdlemg4f  41177  cdlemg8c  41191  cdlemg9a  41194  cdlemg9b  41195  cdlemg10a  41202  cdlemg10  41203  cdlemg12b  41206  cdlemg12f  41210  cdlemg12g  41211  cdlemg12  41212  cdlemg17dN  41225  cdlemg17dALTN  41226  cdlemg17e  41227  cdlemg17f  41228  cdlemg17g  41229  cdlemg17i  41231  cdlemg17ir  41232  cdlemg17pq  41234  cdlemg17bq  41235  cdlemg17iqN  41236  cdlemg17  41239  cdlemg18b  41241  cdlemg18c  41242  cdlemg18d  41243  cdlemg18  41244  cdlemg19  41246  cdlemg21  41248  cdlemg28a  41255  cdlemg31b0a  41257  cdlemg27b  41258  cdlemg33b0  41263  cdlemg28b  41265  cdlemg28  41266  cdlemg35  41275  cdlemg36  41276  cdlemg44a  41293  cdlemh  41379  cdlemi2  41381  cdlemj1  41383  tendocan  41386  cdlemk5a  41397  cdlemk5  41398  cdlemki  41403  cdlemkvcl  41404  cdlemk10  41405  cdlemksv2  41409  cdlemk7  41410  cdlemk11  41411  cdlemk12  41412  cdlemkoatnle  41413  cdlemk15  41417  cdlemk16a  41418  cdlemk16  41419  cdlemk1u  41421  cdlemk5u  41423  cdlemk6u  41424  cdlemk18  41430  cdlemk19  41431  cdlemk7u  41432  cdlemk11u  41433  cdlemk12u  41434  cdlemk21N  41435  cdlemk20  41436  cdlemkoatnle-2N  41437  cdlemk13-2N  41438  cdlemkole-2N  41439  cdlemk14-2N  41440  cdlemk15-2N  41441  cdlemk16-2N  41442  cdlemk17-2N  41443  cdlemk18-2N  41448  cdlemk19-2N  41449  cdlemk22  41455  cdlemk30  41456  cdlemkuel-3  41460  cdlemkuv2-3N  41461  cdlemk18-3N  41462  cdlemkfid1N  41483  cdlemkid1  41484  cdlemkfid3N  41487  cdlemky  41488  cdlemk11ta  41491  cdlemk47  41511  cdlemk48  41512  cdlemk49  41513  cdlemk50  41514  cdlemk51  41515  cdlemk52  41516  cdlemk53a  41517  cdlemk53  41519  cdlemk54  41520  cdlemk55a  41521  cdlemkyyN  41524  cdlemk43N  41525  cdlemk55u1  41527  cdlemk55u  41528  cdlemk39u1  41529  cdlemk19u1  41531  cdleml1N  41538  cdleml2N  41539  cdleml3N  41540  dia2dimlem6  41631  cdlemn2  41757  cdlemn2a  41758  cdlemn5pre  41762  cdlemn11a  41769  dihjustlem  41778  dihjust  41779  dihmeetlem15N  41883  lclkrlem2y  42093  aks6d1c1  42671  relexpmulnn  44223  ormkglobd  47389  natglobalincr  47391  iscnrm3llem1  49508  iscnrm3l  49510  swapffunc  49841  fucofunc  49918  amgmwlem  50361