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  8628  cofsmo  10386  axdc4lem  10572  0catg  17912  funcoppc  18100  funcres  18121  catcisolem  18335  1stfcl  18421  2ndfcl  18422  prfcl  18427  evlfcl  18446  curf1cl  18452  curfcl  18456  hofcl  18483  mulgdirlem  19365  ogrpsub  20402  ogrpaddlt  20403  ogrpsublt  20407  mdetunilem4  22985  mdetuni0  22991  mdetmul  22993  prdsxmetlem  24742  isosctrlem3  27205  isosctr  27206  amgmlem  27374  nosupbnd2lem1  28129  addsass  28448  f1otrg  29505  colinearalg  29545  ax5seglem6  29569  ax5seg  29573  axpasch  29576  axeuclidlem  29597  axeuclid  29598  uhgr2edg  29846  numclwlk1lem2  31028  rhmdvd  33989  bnj1128  35731  mclspps  36557  cgrtr  36972  cgrtr3  36974  ofscom  36987  segconeq  36990  ifscgr  37024  btwnxfr  37036  colinearxfr  37055  lineext  37056  brofs2  37057  brifs2  37058  fscgr  37060  linecgr  37061  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem3  37069  btwnconn1lem4  37070  btwnconn1lem5  37071  btwnconn1lem6  37072  btwnconn1lem7  37073  seglecgr12im  37090  seglecgr12  37091  segletr  37094  broutsideof3  37106  outsideofeq  37110  lineunray  37127  lineelsb2  37128  linecom  37130  lshpkrlem5  40437  omlmod1i2N  40583  cvrnbtwn3  40599  cvrcmp  40606  cvrcmp2  40607  cvlexch2  40652  cvlexchb2  40654  cvlatexchb2  40658  cvlatexch2  40660  cvlatexch3  40661  cvlsupr7  40671  atnlej1  40702  atnlej2  40703  2llnneN  40732  cvratlem  40744  atcvrneN  40753  atcvrj1  40754  atlelt  40761  2atjm  40768  3noncolr2  40772  3noncolr1N  40773  3dimlem2  40782  3dim1  40790  3dim2  40791  1cvrat  40799  ps-1  40800  ps-2  40801  2atjlej  40802  hlatexch3N  40803  ps-2b  40805  3atlem1  40806  3atlem2  40807  3atlem5  40810  3atlem6  40811  llnle  40841  2atm  40850  ps-2c  40851  lplni2  40860  lplnle  40863  lplnnle2at  40864  lplnri3N  40878  llncvrlpln2  40880  2atmat  40884  2llnm2N  40891  2llnm4  40893  2llnmeqat  40894  lvolnle3at  40905  4atlem0ae  40917  4atlem0be  40918  4atlem3b  40921  4atlem9  40926  4atlem10a  40927  4atlem10  40929  4atlem11a  40930  4atlem12a  40933  4at2  40937  2lplnm2N  40944  lneq2at  41101  2llnma1b  41109  2llnma1  41110  2llnma3r  41111  2llnma2  41112  2llnma2rN  41113  cdlema1N  41114  paddasslem2  41144  paddasslem15  41157  paddasslem16  41158  pmodlem1  41169  pmodlem2  41170  pmod2iN  41172  hlmod1i  41179  atmod1i1m  41181  atmod2i1  41184  atmod2i2  41185  atmod3i1  41187  atmod3i2  41188  atmod4i1  41189  atmod4i2  41190  llnexchb2lem  41191  llnexch2N  41193  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem13  41206  dalawlem15  41208  osumcllem9N  41287  pl42lem1N  41302  4atexlems  41375  4atex2  41400  4atex2-0bOLDN  41402  trlval4  41511  cdlemc5  41518  cdlemc6  41519  cdlemd2  41522  cdlemd4  41524  cdlemd6  41526  cdleme00a  41532  cdleme0e  41540  cdleme3g  41557  cdleme3h  41558  cdleme3  41560  cdleme4  41561  cdleme4a  41562  cdleme5  41563  cdleme9  41576  cdleme16aN  41582  cdleme11c  41584  cdleme11e  41586  cdleme11g  41588  cdleme11h  41589  cdleme11j  41590  cdleme11k  41591  cdleme11l  41592  cdleme11  41593  cdleme12  41594  cdleme14  41596  cdleme15c  41599  cdleme16b  41602  cdleme16c  41603  cdleme16d  41604  cdleme16e  41605  cdleme16f  41606  cdleme0nex  41613  cdleme18a  41614  cdleme18c  41616  cdleme18d  41618  cdlemednpq  41622  cdlemednuN  41623  cdleme20zN  41624  cdleme20y  41625  cdleme19a  41626  cdleme19b  41627  cdleme19d  41629  cdleme19e  41630  cdleme20aN  41632  cdleme20bN  41633  cdleme20c  41634  cdleme20d  41635  cdleme20f  41637  cdleme20g  41638  cdleme20i  41640  cdleme20j  41641  cdleme20l1  41643  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme21b  41649  cdleme21c  41650  cdleme21e  41654  cdleme21f  41655  cdleme22a  41663  cdleme22b  41664  cdleme22e  41667  cdleme22eALTN  41668  cdleme22f  41669  cdleme26eALTN  41684  cdleme26fALTN  41685  cdleme26f  41686  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme27N  41692  cdleme28a  41693  cdleme28b  41694  cdleme30a  41701  cdleme43fsv1snlem  41743  cdlemefs31fv1  41747  cdlemefs45eN  41754  cdleme32b  41765  cdleme32c  41766  cdleme32d  41767  cdleme35h  41779  cdleme36a  41783  cdleme36m  41784  cdleme37m  41785  cdleme40m  41790  cdleme40n  41791  cdleme41sn3aw  41797  cdleme41sn4aw  41798  cdleme41fva11  41800  cdleme42k  41807  cdleme43cN  41814  cdleme43dN  41815  cdleme46f2g1  41817  cdlemeg47rv2  41833  cdlemeg46sfg  41843  cdlemeg46fjgN  41844  cdlemeg46rjgN  41845  cdlemeg46fjv  41846  cdlemeg46frv  41848  cdlemeg46vrg  41850  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemeg46gfv  41853  cdlemg4a  41931  cdlemg4d  41936  cdlemg4e  41937  cdlemg4f  41938  cdlemg4g  41939  cdlemg4  41940  cdlemg6d  41944  cdlemg6e  41945  cdlemg8b  41951  cdlemg8c  41952  cdlemg9a  41955  cdlemg9b  41956  cdlemg10a  41963  cdlemg10  41964  cdlemg12a  41966  cdlemg12b  41967  cdlemg12f  41971  cdlemg12g  41972  cdlemg12  41973  cdlemg17dN  41986  cdlemg17dALTN  41987  cdlemg17e  41988  cdlemg17f  41989  cdlemg17g  41990  cdlemg17h  41991  cdlemg17i  41992  cdlemg17pq  41995  cdlemg17iqN  41997  cdlemg17  42000  cdlemg18b  42002  cdlemg18c  42003  cdlemg19a  42006  cdlemg19  42007  cdlemg28a  42016  cdlemg27b  42019  cdlemg28b  42026  cdlemg28  42027  cdlemg33a  42029  cdlemg33b  42030  cdlemg33c  42031  cdlemg33d  42032  cdlemg33e  42033  cdlemg33  42034  cdlemg35  42036  cdlemg36  42037  cdlemg44a  42054  cdlemh  42140  cdlemi2  42142  cdlemj1  42144  tendocan  42147  cdlemk5a  42158  cdlemki  42164  cdlemkvcl  42165  cdlemk10  42166  cdlemksv2  42170  cdlemkole  42176  cdlemk14  42177  cdlemk15  42178  cdlemk16a  42179  cdlemk16  42180  cdlemk17  42181  cdlemk18  42191  cdlemk19  42192  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk30  42217  cdlemk18-3N  42223  cdlemk23-3  42225  cdlemk25-3  42227  cdlemk27-3  42230  cdlemk37  42237  cdlemkfid1N  42244  cdlemkid1  42245  cdlemky  42249  cdlemk11ta  42252  cdlemk47  42272  cdlemk48  42273  cdlemk49  42274  cdlemk50  42275  cdlemk51  42276  cdlemk52  42277  cdlemk53a  42278  cdlemk54  42281  cdlemk39u1  42290  cdlemk19u1  42292  cdleml1N  42299  cdleml2N  42300  cdleml3N  42301  dia2dimlem6  42392  cdlemn2  42518  cdlemn2a  42519  cdlemn5pre  42523  cdlemn10  42529  cdlemn11c  42532  cdlemn11pre  42533  dihjustlem  42539  dihjust  42540  lclkrlem2y  42854  aks6d1c1  43432  relexpmulnn  44970  ormkglobd  48160  lincreslvec3  49925  iscnrm3llem1  50394  iscnrm3l  50396  swapffunc  50735  fucofunc  50812  parmapfunc2  51105  parmapfunc  51106  amgmwlem  51415