Theorem simp21 1207

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8620  cofsmo  10309  axdc4lem  10495  0catg  17731  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  mulgdirlem  19123  mdetunilem4  22621  mdetuni0  22627  mdetmul  22629  prdsxmetlem  24378  isosctrlem3  26863  isosctr  26864  amgmlem  27033  nosupbnd2lem1  27760  addsass  28038  f1otrg  28879  colinearalg  28925  ax5seglem6  28949  ax5seg  28953  axpasch  28956  axeuclidlem  28977  axeuclid  28978  uhgr2edg  29225  numclwlk1lem2  30389  ogrpsub  33093  ogrpaddlt  33094  ogrpsublt  33098  rhmdvd  33348  bnj1128  35004  mclspps  35589  cgrtr  35993  cgrtr3  35995  ofscom  36008  segconeq  36011  ifscgr  36045  btwnxfr  36057  colinearxfr  36076  lineext  36077  brofs2  36078  brifs2  36079  fscgr  36081  linecgr  36082  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  seglecgr12im  36111  seglecgr12  36112  segletr  36115  broutsideof3  36127  outsideofeq  36131  lineunray  36148  lineelsb2  36149  linecom  36151  lshpkrlem5  39115  omlmod1i2N  39261  cvrnbtwn3  39277  cvrcmp  39284  cvrcmp2  39285  cvlexch2  39330  cvlexchb2  39332  cvlatexchb2  39336  cvlatexch2  39338  cvlatexch3  39339  cvlsupr7  39349  atnlej1  39381  atnlej2  39382  2llnneN  39411  cvratlem  39423  atcvrneN  39432  atcvrj1  39433  atlelt  39440  2atjm  39447  3noncolr2  39451  3noncolr1N  39452  3dimlem2  39461  3dim1  39469  3dim2  39470  1cvrat  39478  ps-1  39479  ps-2  39480  2atjlej  39481  hlatexch3N  39482  ps-2b  39484  3atlem1  39485  3atlem2  39486  3atlem5  39489  3atlem6  39490  llnle  39520  2atm  39529  ps-2c  39530  lplni2  39539  lplnle  39542  lplnnle2at  39543  lplnri3N  39557  llncvrlpln2  39559  2atmat  39563  2llnm2N  39570  2llnm4  39572  2llnmeqat  39573  lvolnle3at  39584  4atlem0ae  39596  4atlem0be  39597  4atlem3b  39600  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem12a  39612  4at2  39616  2lplnm2N  39623  lneq2at  39780  2llnma1b  39788  2llnma1  39789  2llnma3r  39790  2llnma2  39791  2llnma2rN  39792  cdlema1N  39793  paddasslem2  39823  paddasslem15  39836  paddasslem16  39837  pmodlem1  39848  pmodlem2  39849  pmod2iN  39851  hlmod1i  39858  atmod1i1m  39860  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  atmod3i2  39867  atmod4i1  39868  atmod4i2  39869  llnexchb2lem  39870  llnexch2N  39872  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem13  39885  dalawlem15  39887  osumcllem9N  39966  pl42lem1N  39981  4atexlems  40054  4atex2  40079  4atex2-0bOLDN  40081  trlval4  40190  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdlemd4  40203  cdlemd6  40205  cdleme00a  40211  cdleme0e  40219  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme4a  40241  cdleme5  40242  cdleme9  40255  cdleme16aN  40261  cdleme11c  40263  cdleme11e  40265  cdleme11g  40267  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme11l  40271  cdleme11  40272  cdleme12  40273  cdleme14  40275  cdleme15c  40278  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme0nex  40292  cdleme18a  40293  cdleme18c  40295  cdleme18d  40297  cdlemednpq  40301  cdlemednuN  40302  cdleme20zN  40303  cdleme20y  40304  cdleme19a  40305  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20aN  40311  cdleme20bN  40312  cdleme20c  40313  cdleme20d  40314  cdleme20f  40316  cdleme20g  40317  cdleme20i  40319  cdleme20j  40320  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21b  40328  cdleme21c  40329  cdleme21e  40333  cdleme21f  40334  cdleme22a  40342  cdleme22b  40343  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme26eALTN  40363  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme30a  40380  cdleme43fsv1snlem  40422  cdlemefs31fv1  40426  cdlemefs45eN  40433  cdleme32b  40444  cdleme32c  40445  cdleme32d  40446  cdleme35h  40458  cdleme36a  40462  cdleme36m  40463  cdleme37m  40464  cdleme40m  40469  cdleme40n  40470  cdleme41sn3aw  40476  cdleme41sn4aw  40477  cdleme41fva11  40479  cdleme42k  40486  cdleme43cN  40493  cdleme43dN  40494  cdleme46f2g1  40496  cdlemeg47rv2  40512  cdlemeg46sfg  40522  cdlemeg46fjgN  40523  cdlemeg46rjgN  40524  cdlemeg46fjv  40525  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdlemg4a  40610  cdlemg4d  40615  cdlemg4e  40616  cdlemg4f  40617  cdlemg4g  40618  cdlemg4  40619  cdlemg6d  40623  cdlemg6e  40624  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg9b  40635  cdlemg10a  40642  cdlemg10  40643  cdlemg12a  40645  cdlemg12b  40646  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg17dN  40665  cdlemg17dALTN  40666  cdlemg17e  40667  cdlemg17f  40668  cdlemg17g  40669  cdlemg17h  40670  cdlemg17i  40671  cdlemg17pq  40674  cdlemg17iqN  40676  cdlemg17  40679  cdlemg18b  40681  cdlemg18c  40682  cdlemg19a  40685  cdlemg19  40686  cdlemg28a  40695  cdlemg27b  40698  cdlemg28b  40705  cdlemg28  40706  cdlemg33a  40708  cdlemg33b  40709  cdlemg33c  40710  cdlemg33d  40711  cdlemg33e  40712  cdlemg33  40713  cdlemg35  40715  cdlemg36  40716  cdlemg44a  40733  cdlemh  40819  cdlemi2  40821  cdlemj1  40823  tendocan  40826  cdlemk5a  40837  cdlemki  40843  cdlemkvcl  40844  cdlemk10  40845  cdlemksv2  40849  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk16a  40858  cdlemk16  40859  cdlemk17  40860  cdlemk18  40870  cdlemk19  40871  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk30  40896  cdlemk18-3N  40902  cdlemk23-3  40904  cdlemk25-3  40906  cdlemk27-3  40909  cdlemk37  40916  cdlemkfid1N  40923  cdlemkid1  40924  cdlemky  40928  cdlemk11ta  40931  cdlemk47  40951  cdlemk48  40952  cdlemk49  40953  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk53a  40957  cdlemk54  40960  cdlemk39u1  40969  cdlemk19u1  40971  cdleml1N  40978  cdleml2N  40979  cdleml3N  40980  dia2dimlem6  41071  cdlemn2  41197  cdlemn2a  41198  cdlemn5pre  41202  cdlemn10  41208  cdlemn11c  41211  cdlemn11pre  41212  dihjustlem  41218  dihjust  41219  lclkrlem2y  41533  aks6d1c1  42117  relexpmulnn  43722  ormkglobd  46890  natglobalincr  46892  lincreslvec3  48399  iscnrm3llem1  48846  iscnrm3l  48848  swapffunc  48988  fucofunc  49054  amgmwlem  49321