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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8503  cofsmo  10166  axdc4lem  10352  0catg  17600  funcoppc  17788  funcres  17809  catcisolem  18023  1stfcl  18109  2ndfcl  18110  prfcl  18115  evlfcl  18134  curf1cl  18140  curfcl  18144  hofcl  18171  mulgdirlem  19024  ogrpsub  20055  ogrpaddlt  20056  ogrpsublt  20060  mdetunilem4  22536  mdetuni0  22542  mdetmul  22544  prdsxmetlem  24289  isosctrlem3  26763  isosctr  26764  amgmlem  26933  nosupbnd2lem1  27660  addsass  27954  f1otrg  28855  colinearalg  28895  ax5seglem6  28919  ax5seg  28923  axpasch  28926  axeuclidlem  28947  axeuclid  28948  uhgr2edg  29193  numclwlk1lem2  30357  rhmdvd  33296  bnj1128  35009  mclspps  35635  cgrtr  36043  cgrtr3  36045  ofscom  36058  segconeq  36061  ifscgr  36095  btwnxfr  36107  colinearxfr  36126  lineext  36127  brofs2  36128  brifs2  36129  fscgr  36131  linecgr  36132  btwnconn1lem1  36138  btwnconn1lem2  36139  btwnconn1lem3  36140  btwnconn1lem4  36141  btwnconn1lem5  36142  btwnconn1lem6  36143  btwnconn1lem7  36144  seglecgr12im  36161  seglecgr12  36162  segletr  36165  broutsideof3  36177  outsideofeq  36181  lineunray  36198  lineelsb2  36199  linecom  36201  lshpkrlem5  39219  omlmod1i2N  39365  cvrnbtwn3  39381  cvrcmp  39388  cvrcmp2  39389  cvlexch2  39434  cvlexchb2  39436  cvlatexchb2  39440  cvlatexch2  39442  cvlatexch3  39443  cvlsupr7  39453  atnlej1  39484  atnlej2  39485  2llnneN  39514  cvratlem  39526  atcvrneN  39535  atcvrj1  39536  atlelt  39543  2atjm  39550  3noncolr2  39554  3noncolr1N  39555  3dimlem2  39564  3dim1  39572  3dim2  39573  1cvrat  39581  ps-1  39582  ps-2  39583  2atjlej  39584  hlatexch3N  39585  ps-2b  39587  3atlem1  39588  3atlem2  39589  3atlem5  39592  3atlem6  39593  llnle  39623  2atm  39632  ps-2c  39633  lplni2  39642  lplnle  39645  lplnnle2at  39646  lplnri3N  39660  llncvrlpln2  39662  2atmat  39666  2llnm2N  39673  2llnm4  39675  2llnmeqat  39676  lvolnle3at  39687  4atlem0ae  39699  4atlem0be  39700  4atlem3b  39703  4atlem9  39708  4atlem10a  39709  4atlem10  39711  4atlem11a  39712  4atlem12a  39715  4at2  39719  2lplnm2N  39726  lneq2at  39883  2llnma1b  39891  2llnma1  39892  2llnma3r  39893  2llnma2  39894  2llnma2rN  39895  cdlema1N  39896  paddasslem2  39926  paddasslem15  39939  paddasslem16  39940  pmodlem1  39951  pmodlem2  39952  pmod2iN  39954  hlmod1i  39961  atmod1i1m  39963  atmod2i1  39966  atmod2i2  39967  atmod3i1  39969  atmod3i2  39970  atmod4i1  39971  atmod4i2  39972  llnexchb2lem  39973  llnexch2N  39975  dalawlem3  39978  dalawlem4  39979  dalawlem5  39980  dalawlem6  39981  dalawlem7  39982  dalawlem8  39983  dalawlem9  39984  dalawlem11  39986  dalawlem12  39987  dalawlem13  39988  dalawlem15  39990  osumcllem9N  40069  pl42lem1N  40084  4atexlems  40157  4atex2  40182  4atex2-0bOLDN  40184  trlval4  40293  cdlemc5  40300  cdlemc6  40301  cdlemd2  40304  cdlemd4  40306  cdlemd6  40308  cdleme00a  40314  cdleme0e  40322  cdleme3g  40339  cdleme3h  40340  cdleme3  40342  cdleme4  40343  cdleme4a  40344  cdleme5  40345  cdleme9  40358  cdleme16aN  40364  cdleme11c  40366  cdleme11e  40368  cdleme11g  40370  cdleme11h  40371  cdleme11j  40372  cdleme11k  40373  cdleme11l  40374  cdleme11  40375  cdleme12  40376  cdleme14  40378  cdleme15c  40381  cdleme16b  40384  cdleme16c  40385  cdleme16d  40386  cdleme16e  40387  cdleme16f  40388  cdleme0nex  40395  cdleme18a  40396  cdleme18c  40398  cdleme18d  40400  cdlemednpq  40404  cdlemednuN  40405  cdleme20zN  40406  cdleme20y  40407  cdleme19a  40408  cdleme19b  40409  cdleme19d  40411  cdleme19e  40412  cdleme20aN  40414  cdleme20bN  40415  cdleme20c  40416  cdleme20d  40417  cdleme20f  40419  cdleme20g  40420  cdleme20i  40422  cdleme20j  40423  cdleme20l1  40425  cdleme20l2  40426  cdleme20l  40427  cdleme20m  40428  cdleme21b  40431  cdleme21c  40432  cdleme21e  40436  cdleme21f  40437  cdleme22a  40445  cdleme22b  40446  cdleme22e  40449  cdleme22eALTN  40450  cdleme22f  40451  cdleme26eALTN  40466  cdleme26fALTN  40467  cdleme26f  40468  cdleme26f2ALTN  40469  cdleme26f2  40470  cdleme27N  40474  cdleme28a  40475  cdleme28b  40476  cdleme30a  40483  cdleme43fsv1snlem  40525  cdlemefs31fv1  40529  cdlemefs45eN  40536  cdleme32b  40547  cdleme32c  40548  cdleme32d  40549  cdleme35h  40561  cdleme36a  40565  cdleme36m  40566  cdleme37m  40567  cdleme40m  40572  cdleme40n  40573  cdleme41sn3aw  40579  cdleme41sn4aw  40580  cdleme41fva11  40582  cdleme42k  40589  cdleme43cN  40596  cdleme43dN  40597  cdleme46f2g1  40599  cdlemeg47rv2  40615  cdlemeg46sfg  40625  cdlemeg46fjgN  40626  cdlemeg46rjgN  40627  cdlemeg46fjv  40628  cdlemeg46frv  40630  cdlemeg46vrg  40632  cdlemeg46rgv  40633  cdlemeg46req  40634  cdlemeg46gfv  40635  cdlemg4a  40713  cdlemg4d  40718  cdlemg4e  40719  cdlemg4f  40720  cdlemg4g  40721  cdlemg4  40722  cdlemg6d  40726  cdlemg6e  40727  cdlemg8b  40733  cdlemg8c  40734  cdlemg9a  40737  cdlemg9b  40738  cdlemg10a  40745  cdlemg10  40746  cdlemg12a  40748  cdlemg12b  40749  cdlemg12f  40753  cdlemg12g  40754  cdlemg12  40755  cdlemg17dN  40768  cdlemg17dALTN  40769  cdlemg17e  40770  cdlemg17f  40771  cdlemg17g  40772  cdlemg17h  40773  cdlemg17i  40774  cdlemg17pq  40777  cdlemg17iqN  40779  cdlemg17  40782  cdlemg18b  40784  cdlemg18c  40785  cdlemg19a  40788  cdlemg19  40789  cdlemg28a  40798  cdlemg27b  40801  cdlemg28b  40808  cdlemg28  40809  cdlemg33a  40811  cdlemg33b  40812  cdlemg33c  40813  cdlemg33d  40814  cdlemg33e  40815  cdlemg33  40816  cdlemg35  40818  cdlemg36  40819  cdlemg44a  40836  cdlemh  40922  cdlemi2  40924  cdlemj1  40926  tendocan  40929  cdlemk5a  40940  cdlemki  40946  cdlemkvcl  40947  cdlemk10  40948  cdlemksv2  40952  cdlemkole  40958  cdlemk14  40959  cdlemk15  40960  cdlemk16a  40961  cdlemk16  40962  cdlemk17  40963  cdlemk18  40973  cdlemk19  40974  cdlemkoatnle-2N  40980  cdlemk13-2N  40981  cdlemkole-2N  40982  cdlemk14-2N  40983  cdlemk15-2N  40984  cdlemk16-2N  40985  cdlemk17-2N  40986  cdlemk18-2N  40991  cdlemk19-2N  40992  cdlemk30  40999  cdlemk18-3N  41005  cdlemk23-3  41007  cdlemk25-3  41009  cdlemk27-3  41012  cdlemk37  41019  cdlemkfid1N  41026  cdlemkid1  41027  cdlemky  41031  cdlemk11ta  41034  cdlemk47  41054  cdlemk48  41055  cdlemk49  41056  cdlemk50  41057  cdlemk51  41058  cdlemk52  41059  cdlemk53a  41060  cdlemk54  41063  cdlemk39u1  41072  cdlemk19u1  41074  cdleml1N  41081  cdleml2N  41082  cdleml3N  41083  dia2dimlem6  41174  cdlemn2  41300  cdlemn2a  41301  cdlemn5pre  41305  cdlemn10  41311  cdlemn11c  41314  cdlemn11pre  41315  dihjustlem  41321  dihjust  41322  lclkrlem2y  41636  aks6d1c1  42215  relexpmulnn  43807  ormkglobd  46978  natglobalincr  46980  lincreslvec3  48588  iscnrm3llem1  49054  iscnrm3l  49056  swapffunc  49388  fucofunc  49465  amgmwlem  49908