Theorem simp22 1203

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 1085

This theorem is referenced by:  simp122  1302  simp222  1311  simp322  1320  elfiun  8897  cofsmo  9694  modexp  13602  funcoppc  17148  funcres  17169  catcisolem  17369  1stfcl  17450  2ndfcl  17451  prfcl  17456  evlfcl  17475  curf1cl  17481  curfcl  17485  hofcl  17512  mulgdirlem  18261  pmtrprfv3  18585  mdetunilem4  21227  mdetuni0  21233  mdetmul  21235  prdsxmetlem  22981  isosctrlem3  25401  isosctr  25402  amgmlem  25570  f1otrg  26660  colinearalg  26699  ax5seglem6  26723  ax5seg  26727  axpasch  26730  axeuclidlem  26751  axeuclid  26752  ogrpsub  30721  ogrpaddlt  30722  ogrpsublt  30726  rhmdvd  30898  bnj966  32220  mclspps  32835  cgrtr  33457  cgrtr3  33459  ofscom  33472  cgrextend  33473  btwnxfr  33521  colinearxfr  33540  lineext  33541  fscgr  33545  linecgr  33546  btwnconn1lem1  33552  btwnconn1lem2  33553  btwnconn1lem3  33554  btwnconn1lem4  33555  btwnconn1lem5  33556  btwnconn1lem6  33557  btwnconn1lem7  33558  seglecgr12im  33575  seglecgr12  33576  segletr  33579  broutsideof3  33591  outsideofeq  33595  lineunray  33612  linecom  33615  eqlkr  36239  lshpkrlem5  36254  omlmod1i2N  36400  cvrnbtwn3  36416  cvrcmp2  36424  cvlexch2  36469  cvlexchb2  36471  cvlatexchb2  36475  cvlatexch1  36476  cvlatexch2  36477  cvlatexch3  36478  cvlsupr7  36488  cvlsupr8  36489  atnlej1  36519  atnlej2  36520  2llnneN  36549  cvratlem  36561  atcvrneN  36570  atlelt  36578  2atjm  36585  3noncolr2  36589  3noncolr1N  36590  hlatcon2  36592  3dimlem2  36599  3dim1  36607  3dim2  36608  1cvrat  36616  ps-1  36617  ps-2  36618  2atjlej  36619  hlatexch3N  36620  ps-2b  36622  3atlem1  36623  3atlem5  36627  3atlem6  36628  2atm  36667  ps-2c  36668  lplni2  36677  lplnri3N  36695  llncvrlpln2  36697  2atmat  36701  2llnm2N  36708  2llnm3N  36709  2llnm4  36710  2llnmeqat  36711  lvolnle3at  36722  4atlem0ae  36734  4atlem0be  36735  4atlem3b  36738  4atlem9  36743  4atlem10a  36744  4atlem10  36746  4atlem11a  36747  4atlem12a  36750  4at2  36754  2lplnm2N  36761  lneq2at  36918  2llnma1b  36926  2llnma1  36927  2llnma3r  36928  2llnma2  36929  2llnma2rN  36930  cdlema1N  36931  paddasslem2  36961  paddasslem16  36975  pmodlem1  36986  pmod2iN  36989  hlmod1i  36996  atmod2i1  37001  atmod2i2  37002  atmod3i1  37004  atmod3i2  37005  atmod4i1  37006  atmod4i2  37007  llnexchb2lem  37008  llnexch2N  37010  dalawlem3  37013  dalawlem4  37014  dalawlem5  37015  dalawlem6  37016  dalawlem7  37017  dalawlem8  37018  dalawlem9  37019  dalawlem11  37021  dalawlem12  37022  dalawlem13  37023  dalawlem15  37025  osumcllem7N  37102  osumcllem9N  37104  pl42lem1N  37119  4atexlemswapqr  37203  4atex2  37217  4atex2-0bOLDN  37219  trlval4  37328  cdlemc5  37335  cdlemc6  37336  cdlemd2  37339  cdlemd4  37341  cdlemd6  37343  cdleme00a  37349  cdleme0e  37357  cdleme4  37378  cdleme4a  37379  cdleme5  37380  cdleme9  37393  cdleme16aN  37399  cdleme11c  37401  cdleme11dN  37402  cdleme11e  37403  cdleme11g  37405  cdleme11h  37406  cdleme11j  37407  cdleme11k  37408  cdleme11l  37409  cdleme11  37410  cdleme12  37411  cdleme13  37412  cdleme14  37413  cdleme15a  37414  cdleme15c  37416  cdleme16b  37419  cdleme16c  37420  cdleme16d  37421  cdleme16e  37422  cdleme16f  37423  cdleme17d1  37429  cdleme0nex  37430  cdleme18a  37431  cdleme18b  37432  cdleme18c  37433  cdleme18d  37435  cdlemednpq  37439  cdlemednuN  37440  cdleme20zN  37441  cdleme20y  37442  cdleme19a  37443  cdleme19b  37444  cdleme19d  37446  cdleme19e  37447  cdleme20aN  37449  cdleme20d  37452  cdleme20f  37454  cdleme20g  37455  cdleme20i  37457  cdleme20j  37458  cdleme20l1  37460  cdleme20l2  37461  cdleme20l  37462  cdleme20m  37463  cdleme21b  37466  cdleme21c  37467  cdleme21e  37471  cdleme21j  37476  cdleme22aa  37479  cdleme22a  37480  cdleme22b  37481  cdleme22cN  37482  cdleme22d  37483  cdleme22e  37484  cdleme22eALTN  37485  cdleme22f  37486  cdleme26fALTN  37502  cdleme26f  37503  cdleme26f2ALTN  37504  cdleme26f2  37505  cdleme27N  37509  cdleme28a  37510  cdleme28b  37511  cdleme30a  37518  cdlemefs31fv1  37564  cdleme32b  37582  cdleme32c  37583  cdleme32e  37585  cdleme35h  37596  cdleme36a  37600  cdleme36m  37601  cdleme41sn3aw  37614  cdleme41sn4aw  37615  cdleme41fva11  37617  cdleme42k  37624  cdleme43cN  37631  cdleme46f2g1  37634  cdlemeg46fjgN  37661  cdlemeg46fjv  37663  cdlemeg46frv  37665  cdlemeg46rgv  37668  cdlemeg46req  37669  cdlemeg46gfv  37670  cdleme50trn2a  37690  cdlemg4a  37748  cdlemg4d  37753  cdlemg4e  37754  cdlemg4f  37755  cdlemg8c  37769  cdlemg9a  37772  cdlemg9b  37773  cdlemg10a  37780  cdlemg10  37781  cdlemg12b  37784  cdlemg12f  37788  cdlemg12g  37789  cdlemg12  37790  cdlemg17dN  37803  cdlemg17dALTN  37804  cdlemg17e  37805  cdlemg17f  37806  cdlemg17g  37807  cdlemg17i  37809  cdlemg17ir  37810  cdlemg17pq  37812  cdlemg17bq  37813  cdlemg17iqN  37814  cdlemg17  37817  cdlemg18b  37819  cdlemg18c  37820  cdlemg18d  37821  cdlemg18  37822  cdlemg19  37824  cdlemg21  37826  cdlemg28a  37833  cdlemg31b0a  37835  cdlemg27b  37836  cdlemg33b0  37841  cdlemg28b  37843  cdlemg28  37844  cdlemg35  37853  cdlemg36  37854  cdlemg44a  37871  cdlemh  37957  cdlemi2  37959  cdlemj1  37961  tendocan  37964  cdlemk5a  37975  cdlemk5  37976  cdlemki  37981  cdlemkvcl  37982  cdlemk10  37983  cdlemksv2  37987  cdlemk7  37988  cdlemk11  37989  cdlemk12  37990  cdlemkoatnle  37991  cdlemk15  37995  cdlemk16a  37996  cdlemk16  37997  cdlemk1u  37999  cdlemk5u  38001  cdlemk6u  38002  cdlemk18  38008  cdlemk19  38009  cdlemk7u  38010  cdlemk11u  38011  cdlemk12u  38012  cdlemk21N  38013  cdlemk20  38014  cdlemkoatnle-2N  38015  cdlemk13-2N  38016  cdlemkole-2N  38017  cdlemk14-2N  38018  cdlemk15-2N  38019  cdlemk16-2N  38020  cdlemk17-2N  38021  cdlemk18-2N  38026  cdlemk19-2N  38027  cdlemk22  38033  cdlemk30  38034  cdlemkuel-3  38038  cdlemkuv2-3N  38039  cdlemk18-3N  38040  cdlemkfid1N  38061  cdlemkid1  38062  cdlemkfid3N  38065  cdlemky  38066  cdlemk11ta  38069  cdlemk47  38089  cdlemk48  38090  cdlemk49  38091  cdlemk50  38092  cdlemk51  38093  cdlemk52  38094  cdlemk53a  38095  cdlemk53  38097  cdlemk54  38098  cdlemk55a  38099  cdlemkyyN  38102  cdlemk43N  38103  cdlemk55u1  38105  cdlemk55u  38106  cdlemk39u1  38107  cdlemk19u1  38109  cdleml1N  38116  cdleml2N  38117  cdleml3N  38118  dia2dimlem6  38209  cdlemn2  38335  cdlemn2a  38336  cdlemn5pre  38340  cdlemn11a  38347  dihjustlem  38356  dihjust  38357  dihmeetlem15N  38461  lclkrlem2y  38671  relexpmulnn  40060  amgmwlem  44910