Theorem simp22 1226

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp122  1325  simp222  1334  simp322  1343  elfiun  9393  cofsmo  10264  modexp  14287  funcoppc  17949  funcres  17970  catcisolem  18184  1stfcl  18270  2ndfcl  18271  prfcl  18276  evlfcl  18295  curf1cl  18301  curfcl  18305  hofcl  18332  mulgdirlem  19194  pmtrprfv3  19547  ogrpsub  20230  ogrpaddlt  20231  ogrpsublt  20235  mdetunilem4  22801  mdetuni0  22807  mdetmul  22809  prdsxmetlem  24554  isosctrlem3  27014  isosctr  27015  amgmlem  27183  f1otrg  29249  colinearalg  29289  ax5seglem6  29313  ax5seg  29317  axpasch  29320  axeuclidlem  29341  axeuclid  29342  rhmdvd  33667  bnj966  35356  mclspps  36089  cgrtr  36497  cgrtr3  36499  ofscom  36512  cgrextend  36513  btwnxfr  36561  colinearxfr  36580  lineext  36581  fscgr  36585  linecgr  36586  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem3  36594  btwnconn1lem4  36595  btwnconn1lem5  36596  btwnconn1lem6  36597  btwnconn1lem7  36598  seglecgr12im  36615  seglecgr12  36616  segletr  36619  broutsideof3  36631  outsideofeq  36635  lineunray  36652  linecom  36655  eqlkr  39906  lshpkrlem5  39921  omlmod1i2N  40067  cvrnbtwn3  40083  cvrcmp2  40091  cvlexch2  40136  cvlexchb2  40138  cvlatexchb2  40142  cvlatexch1  40143  cvlatexch2  40144  cvlatexch3  40145  cvlsupr7  40155  cvlsupr8  40156  atnlej1  40186  atnlej2  40187  2llnneN  40216  cvratlem  40228  atcvrneN  40237  atlelt  40245  2atjm  40252  3noncolr2  40256  3noncolr1N  40257  hlatcon2  40259  3dimlem2  40266  3dim1  40274  3dim2  40275  1cvrat  40283  ps-1  40284  ps-2  40285  2atjlej  40286  hlatexch3N  40287  ps-2b  40289  3atlem1  40290  3atlem5  40294  3atlem6  40295  2atm  40334  ps-2c  40335  lplni2  40344  lplnri3N  40362  llncvrlpln2  40364  2atmat  40368  2llnm2N  40375  2llnm3N  40376  2llnm4  40377  2llnmeqat  40378  lvolnle3at  40389  4atlem0ae  40401  4atlem0be  40402  4atlem3b  40405  4atlem9  40410  4atlem10a  40411  4atlem10  40413  4atlem11a  40414  4atlem12a  40417  4at2  40421  2lplnm2N  40428  lneq2at  40585  2llnma1b  40593  2llnma1  40594  2llnma3r  40595  2llnma2  40596  2llnma2rN  40597  cdlema1N  40598  paddasslem2  40628  paddasslem16  40642  pmodlem1  40653  pmod2iN  40656  hlmod1i  40663  atmod2i1  40668  atmod2i2  40669  atmod3i1  40671  atmod3i2  40672  atmod4i1  40673  atmod4i2  40674  llnexchb2lem  40675  llnexch2N  40677  dalawlem3  40680  dalawlem4  40681  dalawlem5  40682  dalawlem6  40683  dalawlem7  40684  dalawlem8  40685  dalawlem9  40686  dalawlem11  40688  dalawlem12  40689  dalawlem13  40690  dalawlem15  40692  osumcllem7N  40769  osumcllem9N  40771  pl42lem1N  40786  4atexlemswapqr  40870  4atex2  40884  4atex2-0bOLDN  40886  trlval4  40995  cdlemc5  41002  cdlemc6  41003  cdlemd2  41006  cdlemd4  41008  cdlemd6  41010  cdleme00a  41016  cdleme0e  41024  cdleme4  41045  cdleme4a  41046  cdleme5  41047  cdleme9  41060  cdleme16aN  41066  cdleme11c  41068  cdleme11dN  41069  cdleme11e  41070  cdleme11g  41072  cdleme11h  41073  cdleme11j  41074  cdleme11k  41075  cdleme11l  41076  cdleme11  41077  cdleme12  41078  cdleme13  41079  cdleme14  41080  cdleme15a  41081  cdleme15c  41083  cdleme16b  41086  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme17d1  41096  cdleme0nex  41097  cdleme18a  41098  cdleme18b  41099  cdleme18c  41100  cdleme18d  41102  cdlemednpq  41106  cdlemednuN  41107  cdleme20zN  41108  cdleme20y  41109  cdleme19a  41110  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20aN  41116  cdleme20d  41119  cdleme20f  41121  cdleme20g  41122  cdleme20i  41124  cdleme20j  41125  cdleme20l1  41127  cdleme20l2  41128  cdleme20l  41129  cdleme20m  41130  cdleme21b  41133  cdleme21c  41134  cdleme21e  41138  cdleme21j  41143  cdleme22aa  41146  cdleme22a  41147  cdleme22b  41148  cdleme22cN  41149  cdleme22d  41150  cdleme22e  41151  cdleme22eALTN  41152  cdleme22f  41153  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme27N  41176  cdleme28a  41177  cdleme28b  41178  cdleme30a  41185  cdlemefs31fv1  41231  cdleme32b  41249  cdleme32c  41250  cdleme32e  41252  cdleme35h  41263  cdleme36a  41267  cdleme36m  41268  cdleme41sn3aw  41281  cdleme41sn4aw  41282  cdleme41fva11  41284  cdleme42k  41291  cdleme43cN  41298  cdleme46f2g1  41301  cdlemeg46fjgN  41328  cdlemeg46fjv  41330  cdlemeg46frv  41332  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemeg46gfv  41337  cdleme50trn2a  41357  cdlemg4a  41415  cdlemg4d  41420  cdlemg4e  41421  cdlemg4f  41422  cdlemg8c  41436  cdlemg9a  41439  cdlemg9b  41440  cdlemg10a  41447  cdlemg10  41448  cdlemg12b  41451  cdlemg12f  41455  cdlemg12g  41456  cdlemg12  41457  cdlemg17dN  41470  cdlemg17dALTN  41471  cdlemg17e  41472  cdlemg17f  41473  cdlemg17g  41474  cdlemg17i  41476  cdlemg17ir  41477  cdlemg17pq  41479  cdlemg17bq  41480  cdlemg17iqN  41481  cdlemg17  41484  cdlemg18b  41486  cdlemg18c  41487  cdlemg18d  41488  cdlemg18  41489  cdlemg19  41491  cdlemg21  41493  cdlemg28a  41500  cdlemg31b0a  41502  cdlemg27b  41503  cdlemg33b0  41508  cdlemg28b  41510  cdlemg28  41511  cdlemg35  41520  cdlemg36  41521  cdlemg44a  41538  cdlemh  41624  cdlemi2  41626  cdlemj1  41628  tendocan  41631  cdlemk5a  41642  cdlemk5  41643  cdlemki  41648  cdlemkvcl  41649  cdlemk10  41650  cdlemksv2  41654  cdlemk7  41655  cdlemk11  41656  cdlemk12  41657  cdlemkoatnle  41658  cdlemk15  41662  cdlemk16a  41663  cdlemk16  41664  cdlemk1u  41666  cdlemk5u  41668  cdlemk6u  41669  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk11u  41678  cdlemk12u  41679  cdlemk21N  41680  cdlemk20  41681  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk22  41700  cdlemk30  41701  cdlemkuel-3  41705  cdlemkuv2-3N  41706  cdlemk18-3N  41707  cdlemkfid1N  41728  cdlemkid1  41729  cdlemkfid3N  41732  cdlemky  41733  cdlemk11ta  41736  cdlemk47  41756  cdlemk48  41757  cdlemk49  41758  cdlemk50  41759  cdlemk51  41760  cdlemk52  41761  cdlemk53a  41762  cdlemk53  41764  cdlemk54  41765  cdlemk55a  41766  cdlemkyyN  41769  cdlemk43N  41770  cdlemk55u1  41772  cdlemk55u  41773  cdlemk39u1  41774  cdlemk19u1  41776  cdleml1N  41783  cdleml2N  41784  cdleml3N  41785  dia2dimlem6  41876  cdlemn2  42002  cdlemn2a  42003  cdlemn5pre  42007  cdlemn11a  42014  dihjustlem  42023  dihjust  42024  dihmeetlem15N  42128  lclkrlem2y  42338  aks6d1c1  42916  relexpmulnn  44468  ormkglobd  47624  natglobalincr  47626  iscnrm3llem1  49760  iscnrm3l  49762  swapffunc  50093  fucofunc  50170  amgmwlem  50683