Theorem simp21 1206

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 1136	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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 206  df-an 398  df-3an 1089

This theorem is referenced by:  simp121  1305  simp221  1314  simp321  1323  omeulem1  8444  cofsmo  10071  axdc4lem  10257  0catg  17442  funcoppc  17635  funcres  17656  catcisolem  17870  1stfcl  17959  2ndfcl  17960  prfcl  17965  evlfcl  17985  curf1cl  17991  curfcl  17995  hofcl  18022  mulgdirlem  18779  mdetunilem4  21809  mdetuni0  21815  mdetmul  21817  prdsxmetlem  23566  isosctrlem3  26015  isosctr  26016  amgmlem  26184  f1otrg  27277  colinearalg  27323  ax5seglem6  27347  ax5seg  27351  axpasch  27354  axeuclidlem  27375  axeuclid  27376  uhgr2edg  27620  numclwlk1lem2  28779  ogrpsub  31387  ogrpaddlt  31388  ogrpsublt  31392  rhmdvd  31565  bnj1128  33015  mclspps  33591  nosupbnd2lem1  33963  cgrtr  34339  cgrtr3  34341  ofscom  34354  segconeq  34357  ifscgr  34391  btwnxfr  34403  colinearxfr  34422  lineext  34423  brofs2  34424  brifs2  34425  fscgr  34427  linecgr  34428  btwnconn1lem1  34434  btwnconn1lem2  34435  btwnconn1lem3  34436  btwnconn1lem4  34437  btwnconn1lem5  34438  btwnconn1lem6  34439  btwnconn1lem7  34440  seglecgr12im  34457  seglecgr12  34458  segletr  34461  broutsideof3  34473  outsideofeq  34477  lineunray  34494  lineelsb2  34495  linecom  34497  lshpkrlem5  37170  omlmod1i2N  37316  cvrnbtwn3  37332  cvrcmp  37339  cvrcmp2  37340  cvlexch2  37385  cvlexchb2  37387  cvlatexchb2  37391  cvlatexch2  37393  cvlatexch3  37394  cvlsupr7  37404  atnlej1  37435  atnlej2  37436  2llnneN  37465  cvratlem  37477  atcvrneN  37486  atcvrj1  37487  atlelt  37494  2atjm  37501  3noncolr2  37505  3noncolr1N  37506  3dimlem2  37515  3dim1  37523  3dim2  37524  1cvrat  37532  ps-1  37533  ps-2  37534  2atjlej  37535  hlatexch3N  37536  ps-2b  37538  3atlem1  37539  3atlem2  37540  3atlem5  37543  3atlem6  37544  llnle  37574  2atm  37583  ps-2c  37584  lplni2  37593  lplnle  37596  lplnnle2at  37597  lplnri3N  37611  llncvrlpln2  37613  2atmat  37617  2llnm2N  37624  2llnm4  37626  2llnmeqat  37627  lvolnle3at  37638  4atlem0ae  37650  4atlem0be  37651  4atlem3b  37654  4atlem9  37659  4atlem10a  37660  4atlem10  37662  4atlem11a  37663  4atlem12a  37666  4at2  37670  2lplnm2N  37677  lneq2at  37834  2llnma1b  37842  2llnma1  37843  2llnma3r  37844  2llnma2  37845  2llnma2rN  37846  cdlema1N  37847  paddasslem2  37877  paddasslem15  37890  paddasslem16  37891  pmodlem1  37902  pmodlem2  37903  pmod2iN  37905  hlmod1i  37912  atmod1i1m  37914  atmod2i1  37917  atmod2i2  37918  atmod3i1  37920  atmod3i2  37921  atmod4i1  37922  atmod4i2  37923  llnexchb2lem  37924  llnexch2N  37926  dalawlem3  37929  dalawlem4  37930  dalawlem5  37931  dalawlem6  37932  dalawlem7  37933  dalawlem8  37934  dalawlem9  37935  dalawlem11  37937  dalawlem12  37938  dalawlem13  37939  dalawlem15  37941  osumcllem9N  38020  pl42lem1N  38035  4atexlems  38108  4atex2  38133  4atex2-0bOLDN  38135  trlval4  38244  cdlemc5  38251  cdlemc6  38252  cdlemd2  38255  cdlemd4  38257  cdlemd6  38259  cdleme00a  38265  cdleme0e  38273  cdleme3g  38290  cdleme3h  38291  cdleme3  38293  cdleme4  38294  cdleme4a  38295  cdleme5  38296  cdleme9  38309  cdleme16aN  38315  cdleme11c  38317  cdleme11e  38319  cdleme11g  38321  cdleme11h  38322  cdleme11j  38323  cdleme11k  38324  cdleme11l  38325  cdleme11  38326  cdleme12  38327  cdleme14  38329  cdleme15c  38332  cdleme16b  38335  cdleme16c  38336  cdleme16d  38337  cdleme16e  38338  cdleme16f  38339  cdleme0nex  38346  cdleme18a  38347  cdleme18c  38349  cdleme18d  38351  cdlemednpq  38355  cdlemednuN  38356  cdleme20zN  38357  cdleme20y  38358  cdleme19a  38359  cdleme19b  38360  cdleme19d  38362  cdleme19e  38363  cdleme20aN  38365  cdleme20bN  38366  cdleme20c  38367  cdleme20d  38368  cdleme20f  38370  cdleme20g  38371  cdleme20i  38373  cdleme20j  38374  cdleme20l1  38376  cdleme20l2  38377  cdleme20l  38378  cdleme20m  38379  cdleme21b  38382  cdleme21c  38383  cdleme21e  38387  cdleme21f  38388  cdleme22a  38396  cdleme22b  38397  cdleme22e  38400  cdleme22eALTN  38401  cdleme22f  38402  cdleme26eALTN  38417  cdleme26fALTN  38418  cdleme26f  38419  cdleme26f2ALTN  38420  cdleme26f2  38421  cdleme27N  38425  cdleme28a  38426  cdleme28b  38427  cdleme30a  38434  cdleme43fsv1snlem  38476  cdlemefs31fv1  38480  cdlemefs45eN  38487  cdleme32b  38498  cdleme32c  38499  cdleme32d  38500  cdleme35h  38512  cdleme36a  38516  cdleme36m  38517  cdleme37m  38518  cdleme40m  38523  cdleme40n  38524  cdleme41sn3aw  38530  cdleme41sn4aw  38531  cdleme41fva11  38533  cdleme42k  38540  cdleme43cN  38547  cdleme43dN  38548  cdleme46f2g1  38550  cdlemeg47rv2  38566  cdlemeg46sfg  38576  cdlemeg46fjgN  38577  cdlemeg46rjgN  38578  cdlemeg46fjv  38579  cdlemeg46frv  38581  cdlemeg46vrg  38583  cdlemeg46rgv  38584  cdlemeg46req  38585  cdlemeg46gfv  38586  cdlemg4a  38664  cdlemg4d  38669  cdlemg4e  38670  cdlemg4f  38671  cdlemg4g  38672  cdlemg4  38673  cdlemg6d  38677  cdlemg6e  38678  cdlemg8b  38684  cdlemg8c  38685  cdlemg9a  38688  cdlemg9b  38689  cdlemg10a  38696  cdlemg10  38697  cdlemg12a  38699  cdlemg12b  38700  cdlemg12f  38704  cdlemg12g  38705  cdlemg12  38706  cdlemg17dN  38719  cdlemg17dALTN  38720  cdlemg17e  38721  cdlemg17f  38722  cdlemg17g  38723  cdlemg17h  38724  cdlemg17i  38725  cdlemg17pq  38728  cdlemg17iqN  38730  cdlemg17  38733  cdlemg18b  38735  cdlemg18c  38736  cdlemg19a  38739  cdlemg19  38740  cdlemg28a  38749  cdlemg27b  38752  cdlemg28b  38759  cdlemg28  38760  cdlemg33a  38762  cdlemg33b  38763  cdlemg33c  38764  cdlemg33d  38765  cdlemg33e  38766  cdlemg33  38767  cdlemg35  38769  cdlemg36  38770  cdlemg44a  38787  cdlemh  38873  cdlemi2  38875  cdlemj1  38877  tendocan  38880  cdlemk5a  38891  cdlemki  38897  cdlemkvcl  38898  cdlemk10  38899  cdlemksv2  38903  cdlemkole  38909  cdlemk14  38910  cdlemk15  38911  cdlemk16a  38912  cdlemk16  38913  cdlemk17  38914  cdlemk18  38924  cdlemk19  38925  cdlemkoatnle-2N  38931  cdlemk13-2N  38932  cdlemkole-2N  38933  cdlemk14-2N  38934  cdlemk15-2N  38935  cdlemk16-2N  38936  cdlemk17-2N  38937  cdlemk18-2N  38942  cdlemk19-2N  38943  cdlemk30  38950  cdlemk18-3N  38956  cdlemk23-3  38958  cdlemk25-3  38960  cdlemk27-3  38963  cdlemk37  38970  cdlemkfid1N  38977  cdlemkid1  38978  cdlemky  38982  cdlemk11ta  38985  cdlemk47  39005  cdlemk48  39006  cdlemk49  39007  cdlemk50  39008  cdlemk51  39009  cdlemk52  39010  cdlemk53a  39011  cdlemk54  39014  cdlemk39u1  39023  cdlemk19u1  39025  cdleml1N  39032  cdleml2N  39033  cdleml3N  39034  dia2dimlem6  39125  cdlemn2  39251  cdlemn2a  39252  cdlemn5pre  39256  cdlemn10  39262  cdlemn11c  39265  cdlemn11pre  39266  dihjustlem  39272  dihjust  39273  lclkrlem2y  39587  relexpmulnn  41355  lincreslvec3  45881  iscnrm3llem1  46301  iscnrm3l  46303  amgmwlem  46564  natglobalincr  46570