Theorem simp21 1225

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp21	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp21

Step	Hyp	Ref	Expression
1		simp1 1154	. 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:  simp121  1324  simp221  1333  simp321  1342  omeulem1  8569  cofsmo  10264  axdc4lem  10450  0catg  17761  funcoppc  17949  funcres  17970  catcisolem  18184  1stfcl  18270  2ndfcl  18271  prfcl  18276  evlfcl  18295  curf1cl  18301  curfcl  18305  hofcl  18332  mulgdirlem  19194  ogrpsub  20230  ogrpaddlt  20231  ogrpsublt  20235  mdetunilem4  22801  mdetuni0  22807  mdetmul  22809  prdsxmetlem  24554  isosctrlem3  27014  isosctr  27015  amgmlem  27183  nosupbnd2lem1  27908  addsass  28227  f1otrg  29249  colinearalg  29289  ax5seglem6  29313  ax5seg  29317  axpasch  29320  axeuclidlem  29341  axeuclid  29342  uhgr2edg  29587  numclwlk1lem2  30750  rhmdvd  33667  bnj1128  35402  mclspps  36089  cgrtr  36497  cgrtr3  36499  ofscom  36512  segconeq  36515  ifscgr  36549  btwnxfr  36561  colinearxfr  36580  lineext  36581  brofs2  36582  brifs2  36583  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  lineelsb2  36653  linecom  36655  lshpkrlem5  39921  omlmod1i2N  40067  cvrnbtwn3  40083  cvrcmp  40090  cvrcmp2  40091  cvlexch2  40136  cvlexchb2  40138  cvlatexchb2  40142  cvlatexch2  40144  cvlatexch3  40145  cvlsupr7  40155  atnlej1  40186  atnlej2  40187  2llnneN  40216  cvratlem  40228  atcvrneN  40237  atcvrj1  40238  atlelt  40245  2atjm  40252  3noncolr2  40256  3noncolr1N  40257  3dimlem2  40266  3dim1  40274  3dim2  40275  1cvrat  40283  ps-1  40284  ps-2  40285  2atjlej  40286  hlatexch3N  40287  ps-2b  40289  3atlem1  40290  3atlem2  40291  3atlem5  40294  3atlem6  40295  llnle  40325  2atm  40334  ps-2c  40335  lplni2  40344  lplnle  40347  lplnnle2at  40348  lplnri3N  40362  llncvrlpln2  40364  2atmat  40368  2llnm2N  40375  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  paddasslem15  40641  paddasslem16  40642  pmodlem1  40653  pmodlem2  40654  pmod2iN  40656  hlmod1i  40663  atmod1i1m  40665  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  osumcllem9N  40771  pl42lem1N  40786  4atexlems  40859  4atex2  40884  4atex2-0bOLDN  40886  trlval4  40995  cdlemc5  41002  cdlemc6  41003  cdlemd2  41006  cdlemd4  41008  cdlemd6  41010  cdleme00a  41016  cdleme0e  41024  cdleme3g  41041  cdleme3h  41042  cdleme3  41044  cdleme4  41045  cdleme4a  41046  cdleme5  41047  cdleme9  41060  cdleme16aN  41066  cdleme11c  41068  cdleme11e  41070  cdleme11g  41072  cdleme11h  41073  cdleme11j  41074  cdleme11k  41075  cdleme11l  41076  cdleme11  41077  cdleme12  41078  cdleme14  41080  cdleme15c  41083  cdleme16b  41086  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme0nex  41097  cdleme18a  41098  cdleme18c  41100  cdleme18d  41102  cdlemednpq  41106  cdlemednuN  41107  cdleme20zN  41108  cdleme20y  41109  cdleme19a  41110  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20aN  41116  cdleme20bN  41117  cdleme20c  41118  cdleme20d  41119  cdleme20f  41121  cdleme20g  41122  cdleme20i  41124  cdleme20j  41125  cdleme20l1  41127  cdleme20l2  41128  cdleme20l  41129  cdleme20m  41130  cdleme21b  41133  cdleme21c  41134  cdleme21e  41138  cdleme21f  41139  cdleme22a  41147  cdleme22b  41148  cdleme22e  41151  cdleme22eALTN  41152  cdleme22f  41153  cdleme26eALTN  41168  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme27N  41176  cdleme28a  41177  cdleme28b  41178  cdleme30a  41185  cdleme43fsv1snlem  41227  cdlemefs31fv1  41231  cdlemefs45eN  41238  cdleme32b  41249  cdleme32c  41250  cdleme32d  41251  cdleme35h  41263  cdleme36a  41267  cdleme36m  41268  cdleme37m  41269  cdleme40m  41274  cdleme40n  41275  cdleme41sn3aw  41281  cdleme41sn4aw  41282  cdleme41fva11  41284  cdleme42k  41291  cdleme43cN  41298  cdleme43dN  41299  cdleme46f2g1  41301  cdlemeg47rv2  41317  cdlemeg46sfg  41327  cdlemeg46fjgN  41328  cdlemeg46rjgN  41329  cdlemeg46fjv  41330  cdlemeg46frv  41332  cdlemeg46vrg  41334  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemeg46gfv  41337  cdlemg4a  41415  cdlemg4d  41420  cdlemg4e  41421  cdlemg4f  41422  cdlemg4g  41423  cdlemg4  41424  cdlemg6d  41428  cdlemg6e  41429  cdlemg8b  41435  cdlemg8c  41436  cdlemg9a  41439  cdlemg9b  41440  cdlemg10a  41447  cdlemg10  41448  cdlemg12a  41450  cdlemg12b  41451  cdlemg12f  41455  cdlemg12g  41456  cdlemg12  41457  cdlemg17dN  41470  cdlemg17dALTN  41471  cdlemg17e  41472  cdlemg17f  41473  cdlemg17g  41474  cdlemg17h  41475  cdlemg17i  41476  cdlemg17pq  41479  cdlemg17iqN  41481  cdlemg17  41484  cdlemg18b  41486  cdlemg18c  41487  cdlemg19a  41490  cdlemg19  41491  cdlemg28a  41500  cdlemg27b  41503  cdlemg28b  41510  cdlemg28  41511  cdlemg33a  41513  cdlemg33b  41514  cdlemg33c  41515  cdlemg33d  41516  cdlemg33e  41517  cdlemg33  41518  cdlemg35  41520  cdlemg36  41521  cdlemg44a  41538  cdlemh  41624  cdlemi2  41626  cdlemj1  41628  tendocan  41631  cdlemk5a  41642  cdlemki  41648  cdlemkvcl  41649  cdlemk10  41650  cdlemksv2  41654  cdlemkole  41660  cdlemk14  41661  cdlemk15  41662  cdlemk16a  41663  cdlemk16  41664  cdlemk17  41665  cdlemk18  41675  cdlemk19  41676  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  cdlemk30  41701  cdlemk18-3N  41707  cdlemk23-3  41709  cdlemk25-3  41711  cdlemk27-3  41714  cdlemk37  41721  cdlemkfid1N  41728  cdlemkid1  41729  cdlemky  41733  cdlemk11ta  41736  cdlemk47  41756  cdlemk48  41757  cdlemk49  41758  cdlemk50  41759  cdlemk51  41760  cdlemk52  41761  cdlemk53a  41762  cdlemk54  41765  cdlemk39u1  41774  cdlemk19u1  41776  cdleml1N  41783  cdleml2N  41784  cdleml3N  41785  dia2dimlem6  41876  cdlemn2  42002  cdlemn2a  42003  cdlemn5pre  42007  cdlemn10  42013  cdlemn11c  42016  cdlemn11pre  42017  dihjustlem  42023  dihjust  42024  lclkrlem2y  42338  aks6d1c1  42916  relexpmulnn  44468  ormkglobd  47624  natglobalincr  47626  lincreslvec3  49295  iscnrm3llem1  49760  iscnrm3l  49762  swapffunc  50093  fucofunc  50170  amgmwlem  50683