Theorem simp21 1224

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

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

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 401  df-3an 1104

This theorem is used by:  simp121  1323  simp221  1332  simp321  1341  omeulem1  8565  cofsmo  10259  axdc4lem  10445  0catg  17750  funcoppc  17938  funcres  17959  catcisolem  18173  1stfcl  18259  2ndfcl  18260  prfcl  18265  evlfcl  18284  curf1cl  18290  curfcl  18294  hofcl  18321  mulgdirlem  19177  ogrpsub  20213  ogrpaddlt  20214  ogrpsublt  20218  mdetunilem4  22783  mdetuni0  22789  mdetmul  22791  prdsxmetlem  24536  isosctrlem3  26996  isosctr  26997  amgmlem  27165  nosupbnd2lem1  27890  addsass  28209  f1otrg  29231  colinearalg  29271  ax5seglem6  29295  ax5seg  29299  axpasch  29302  axeuclidlem  29323  axeuclid  29324  uhgr2edg  29569  numclwlk1lem2  30732  rhmdvd  33653  bnj1128  35387  mclspps  36084  cgrtr  36492  cgrtr3  36494  ofscom  36507  segconeq  36510  ifscgr  36544  btwnxfr  36556  colinearxfr  36575  lineext  36576  brofs2  36577  brifs2  36578  fscgr  36580  linecgr  36581  btwnconn1lem1  36587  btwnconn1lem2  36588  btwnconn1lem3  36589  btwnconn1lem4  36590  btwnconn1lem5  36591  btwnconn1lem6  36592  btwnconn1lem7  36593  seglecgr12im  36610  seglecgr12  36611  segletr  36614  broutsideof3  36626  outsideofeq  36630  lineunray  36647  lineelsb2  36648  linecom  36650  lshpkrlem5  39916  omlmod1i2N  40062  cvrnbtwn3  40078  cvrcmp  40085  cvrcmp2  40086  cvlexch2  40131  cvlexchb2  40133  cvlatexchb2  40137  cvlatexch2  40139  cvlatexch3  40140  cvlsupr7  40150  atnlej1  40181  atnlej2  40182  2llnneN  40211  cvratlem  40223  atcvrneN  40232  atcvrj1  40233  atlelt  40240  2atjm  40247  3noncolr2  40251  3noncolr1N  40252  3dimlem2  40261  3dim1  40269  3dim2  40270  1cvrat  40278  ps-1  40279  ps-2  40280  2atjlej  40281  hlatexch3N  40282  ps-2b  40284  3atlem1  40285  3atlem2  40286  3atlem5  40289  3atlem6  40290  llnle  40320  2atm  40329  ps-2c  40330  lplni2  40339  lplnle  40342  lplnnle2at  40343  lplnri3N  40357  llncvrlpln2  40359  2atmat  40363  2llnm2N  40370  2llnm4  40372  2llnmeqat  40373  lvolnle3at  40384  4atlem0ae  40396  4atlem0be  40397  4atlem3b  40400  4atlem9  40405  4atlem10a  40406  4atlem10  40408  4atlem11a  40409  4atlem12a  40412  4at2  40416  2lplnm2N  40423  lneq2at  40580  2llnma1b  40588  2llnma1  40589  2llnma3r  40590  2llnma2  40591  2llnma2rN  40592  cdlema1N  40593  paddasslem2  40623  paddasslem15  40636  paddasslem16  40637  pmodlem1  40648  pmodlem2  40649  pmod2iN  40651  hlmod1i  40658  atmod1i1m  40660  atmod2i1  40663  atmod2i2  40664  atmod3i1  40666  atmod3i2  40667  atmod4i1  40668  atmod4i2  40669  llnexchb2lem  40670  llnexch2N  40672  dalawlem3  40675  dalawlem4  40676  dalawlem5  40677  dalawlem6  40678  dalawlem7  40679  dalawlem8  40680  dalawlem9  40681  dalawlem11  40683  dalawlem12  40684  dalawlem13  40685  dalawlem15  40687  osumcllem9N  40766  pl42lem1N  40781  4atexlems  40854  4atex2  40879  4atex2-0bOLDN  40881  trlval4  40990  cdlemc5  40997  cdlemc6  40998  cdlemd2  41001  cdlemd4  41003  cdlemd6  41005  cdleme00a  41011  cdleme0e  41019  cdleme3g  41036  cdleme3h  41037  cdleme3  41039  cdleme4  41040  cdleme4a  41041  cdleme5  41042  cdleme9  41055  cdleme16aN  41061  cdleme11c  41063  cdleme11e  41065  cdleme11g  41067  cdleme11h  41068  cdleme11j  41069  cdleme11k  41070  cdleme11l  41071  cdleme11  41072  cdleme12  41073  cdleme14  41075  cdleme15c  41078  cdleme16b  41081  cdleme16c  41082  cdleme16d  41083  cdleme16e  41084  cdleme16f  41085  cdleme0nex  41092  cdleme18a  41093  cdleme18c  41095  cdleme18d  41097  cdlemednpq  41101  cdlemednuN  41102  cdleme20zN  41103  cdleme20y  41104  cdleme19a  41105  cdleme19b  41106  cdleme19d  41108  cdleme19e  41109  cdleme20aN  41111  cdleme20bN  41112  cdleme20c  41113  cdleme20d  41114  cdleme20f  41116  cdleme20g  41117  cdleme20i  41119  cdleme20j  41120  cdleme20l1  41122  cdleme20l2  41123  cdleme20l  41124  cdleme20m  41125  cdleme21b  41128  cdleme21c  41129  cdleme21e  41133  cdleme21f  41134  cdleme22a  41142  cdleme22b  41143  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme26eALTN  41163  cdleme26fALTN  41164  cdleme26f  41165  cdleme26f2ALTN  41166  cdleme26f2  41167  cdleme27N  41171  cdleme28a  41172  cdleme28b  41173  cdleme30a  41180  cdleme43fsv1snlem  41222  cdlemefs31fv1  41226  cdlemefs45eN  41233  cdleme32b  41244  cdleme32c  41245  cdleme32d  41246  cdleme35h  41258  cdleme36a  41262  cdleme36m  41263  cdleme37m  41264  cdleme40m  41269  cdleme40n  41270  cdleme41sn3aw  41276  cdleme41sn4aw  41277  cdleme41fva11  41279  cdleme42k  41286  cdleme43cN  41293  cdleme43dN  41294  cdleme46f2g1  41296  cdlemeg47rv2  41312  cdlemeg46sfg  41322  cdlemeg46fjgN  41323  cdlemeg46rjgN  41324  cdlemeg46fjv  41325  cdlemeg46frv  41327  cdlemeg46vrg  41329  cdlemeg46rgv  41330  cdlemeg46req  41331  cdlemeg46gfv  41332  cdlemg4a  41410  cdlemg4d  41415  cdlemg4e  41416  cdlemg4f  41417  cdlemg4g  41418  cdlemg4  41419  cdlemg6d  41423  cdlemg6e  41424  cdlemg8b  41430  cdlemg8c  41431  cdlemg9a  41434  cdlemg9b  41435  cdlemg10a  41442  cdlemg10  41443  cdlemg12a  41445  cdlemg12b  41446  cdlemg12f  41450  cdlemg12g  41451  cdlemg12  41452  cdlemg17dN  41465  cdlemg17dALTN  41466  cdlemg17e  41467  cdlemg17f  41468  cdlemg17g  41469  cdlemg17h  41470  cdlemg17i  41471  cdlemg17pq  41474  cdlemg17iqN  41476  cdlemg17  41479  cdlemg18b  41481  cdlemg18c  41482  cdlemg19a  41485  cdlemg19  41486  cdlemg28a  41495  cdlemg27b  41498  cdlemg28b  41505  cdlemg28  41506  cdlemg33a  41508  cdlemg33b  41509  cdlemg33c  41510  cdlemg33d  41511  cdlemg33e  41512  cdlemg33  41513  cdlemg35  41515  cdlemg36  41516  cdlemg44a  41533  cdlemh  41619  cdlemi2  41621  cdlemj1  41623  tendocan  41626  cdlemk5a  41637  cdlemki  41643  cdlemkvcl  41644  cdlemk10  41645  cdlemksv2  41649  cdlemkole  41655  cdlemk14  41656  cdlemk15  41657  cdlemk16a  41658  cdlemk16  41659  cdlemk17  41660  cdlemk18  41670  cdlemk19  41671  cdlemkoatnle-2N  41677  cdlemk13-2N  41678  cdlemkole-2N  41679  cdlemk14-2N  41680  cdlemk15-2N  41681  cdlemk16-2N  41682  cdlemk17-2N  41683  cdlemk18-2N  41688  cdlemk19-2N  41689  cdlemk30  41696  cdlemk18-3N  41702  cdlemk23-3  41704  cdlemk25-3  41706  cdlemk27-3  41709  cdlemk37  41716  cdlemkfid1N  41723  cdlemkid1  41724  cdlemky  41728  cdlemk11ta  41731  cdlemk47  41751  cdlemk48  41752  cdlemk49  41753  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  cdlemk53a  41757  cdlemk54  41760  cdlemk39u1  41769  cdlemk19u1  41771  cdleml1N  41778  cdleml2N  41779  cdleml3N  41780  dia2dimlem6  41871  cdlemn2  41997  cdlemn2a  41998  cdlemn5pre  42002  cdlemn10  42008  cdlemn11c  42011  cdlemn11pre  42012  dihjustlem  42018  dihjust  42019  lclkrlem2y  42333  aks6d1c1  42911  relexpmulnn  44463  ormkglobd  47619  natglobalincr  47621  lincreslvec3  49290  iscnrm3llem1  49755  iscnrm3l  49757  swapffunc  50088  fucofunc  50165  amgmwlem  50677