Theorem simp21 1213

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp121  1312  simp221  1321  simp321  1330  omeulem1  8507  cofsmo  10182  axdc4lem  10368  0catg  17645  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  mulgdirlem  19072  ogrpsub  20103  ogrpaddlt  20104  ogrpsublt  20108  mdetunilem4  22598  mdetuni0  22604  mdetmul  22606  prdsxmetlem  24351  isosctrlem3  26802  isosctr  26803  amgmlem  26971  nosupbnd2lem1  27697  addsass  28015  f1otrg  28957  colinearalg  28997  ax5seglem6  29021  ax5seg  29025  axpasch  29028  axeuclidlem  29049  axeuclid  29050  uhgr2edg  29295  numclwlk1lem2  30458  rhmdvd  33407  bnj1128  35172  mclspps  35812  cgrtr  36220  cgrtr3  36222  ofscom  36235  segconeq  36238  ifscgr  36272  btwnxfr  36284  colinearxfr  36303  lineext  36304  brofs2  36305  brifs2  36306  fscgr  36308  linecgr  36309  btwnconn1lem1  36315  btwnconn1lem2  36316  btwnconn1lem3  36317  btwnconn1lem4  36318  btwnconn1lem5  36319  btwnconn1lem6  36320  btwnconn1lem7  36321  seglecgr12im  36338  seglecgr12  36339  segletr  36342  broutsideof3  36354  outsideofeq  36358  lineunray  36375  lineelsb2  36376  linecom  36378  lshpkrlem5  39606  omlmod1i2N  39752  cvrnbtwn3  39768  cvrcmp  39775  cvrcmp2  39776  cvlexch2  39821  cvlexchb2  39823  cvlatexchb2  39827  cvlatexch2  39829  cvlatexch3  39830  cvlsupr7  39840  atnlej1  39871  atnlej2  39872  2llnneN  39901  cvratlem  39913  atcvrneN  39922  atcvrj1  39923  atlelt  39930  2atjm  39937  3noncolr2  39941  3noncolr1N  39942  3dimlem2  39951  3dim1  39959  3dim2  39960  1cvrat  39968  ps-1  39969  ps-2  39970  2atjlej  39971  hlatexch3N  39972  ps-2b  39974  3atlem1  39975  3atlem2  39976  3atlem5  39979  3atlem6  39980  llnle  40010  2atm  40019  ps-2c  40020  lplni2  40029  lplnle  40032  lplnnle2at  40033  lplnri3N  40047  llncvrlpln2  40049  2atmat  40053  2llnm2N  40060  2llnm4  40062  2llnmeqat  40063  lvolnle3at  40074  4atlem0ae  40086  4atlem0be  40087  4atlem3b  40090  4atlem9  40095  4atlem10a  40096  4atlem10  40098  4atlem11a  40099  4atlem12a  40102  4at2  40106  2lplnm2N  40113  lneq2at  40270  2llnma1b  40278  2llnma1  40279  2llnma3r  40280  2llnma2  40281  2llnma2rN  40282  cdlema1N  40283  paddasslem2  40313  paddasslem15  40326  paddasslem16  40327  pmodlem1  40338  pmodlem2  40339  pmod2iN  40341  hlmod1i  40348  atmod1i1m  40350  atmod2i1  40353  atmod2i2  40354  atmod3i1  40356  atmod3i2  40357  atmod4i1  40358  atmod4i2  40359  llnexchb2lem  40360  llnexch2N  40362  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem13  40375  dalawlem15  40377  osumcllem9N  40456  pl42lem1N  40471  4atexlems  40544  4atex2  40569  4atex2-0bOLDN  40571  trlval4  40680  cdlemc5  40687  cdlemc6  40688  cdlemd2  40691  cdlemd4  40693  cdlemd6  40695  cdleme00a  40701  cdleme0e  40709  cdleme3g  40726  cdleme3h  40727  cdleme3  40729  cdleme4  40730  cdleme4a  40731  cdleme5  40732  cdleme9  40745  cdleme16aN  40751  cdleme11c  40753  cdleme11e  40755  cdleme11g  40757  cdleme11h  40758  cdleme11j  40759  cdleme11k  40760  cdleme11l  40761  cdleme11  40762  cdleme12  40763  cdleme14  40765  cdleme15c  40768  cdleme16b  40771  cdleme16c  40772  cdleme16d  40773  cdleme16e  40774  cdleme16f  40775  cdleme0nex  40782  cdleme18a  40783  cdleme18c  40785  cdleme18d  40787  cdlemednpq  40791  cdlemednuN  40792  cdleme20zN  40793  cdleme20y  40794  cdleme19a  40795  cdleme19b  40796  cdleme19d  40798  cdleme19e  40799  cdleme20aN  40801  cdleme20bN  40802  cdleme20c  40803  cdleme20d  40804  cdleme20f  40806  cdleme20g  40807  cdleme20i  40809  cdleme20j  40810  cdleme20l1  40812  cdleme20l2  40813  cdleme20l  40814  cdleme20m  40815  cdleme21b  40818  cdleme21c  40819  cdleme21e  40823  cdleme21f  40824  cdleme22a  40832  cdleme22b  40833  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f  40838  cdleme26eALTN  40853  cdleme26fALTN  40854  cdleme26f  40855  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme27N  40861  cdleme28a  40862  cdleme28b  40863  cdleme30a  40870  cdleme43fsv1snlem  40912  cdlemefs31fv1  40916  cdlemefs45eN  40923  cdleme32b  40934  cdleme32c  40935  cdleme32d  40936  cdleme35h  40948  cdleme36a  40952  cdleme36m  40953  cdleme37m  40954  cdleme40m  40959  cdleme40n  40960  cdleme41sn3aw  40966  cdleme41sn4aw  40967  cdleme41fva11  40969  cdleme42k  40976  cdleme43cN  40983  cdleme43dN  40984  cdleme46f2g1  40986  cdlemeg47rv2  41002  cdlemeg46sfg  41012  cdlemeg46fjgN  41013  cdlemeg46rjgN  41014  cdlemeg46fjv  41015  cdlemeg46frv  41017  cdlemeg46vrg  41019  cdlemeg46rgv  41020  cdlemeg46req  41021  cdlemeg46gfv  41022  cdlemg4a  41100  cdlemg4d  41105  cdlemg4e  41106  cdlemg4f  41107  cdlemg4g  41108  cdlemg4  41109  cdlemg6d  41113  cdlemg6e  41114  cdlemg8b  41120  cdlemg8c  41121  cdlemg9a  41124  cdlemg9b  41125  cdlemg10a  41132  cdlemg10  41133  cdlemg12a  41135  cdlemg12b  41136  cdlemg12f  41140  cdlemg12g  41141  cdlemg12  41142  cdlemg17dN  41155  cdlemg17dALTN  41156  cdlemg17e  41157  cdlemg17f  41158  cdlemg17g  41159  cdlemg17h  41160  cdlemg17i  41161  cdlemg17pq  41164  cdlemg17iqN  41166  cdlemg17  41169  cdlemg18b  41171  cdlemg18c  41172  cdlemg19a  41175  cdlemg19  41176  cdlemg28a  41185  cdlemg27b  41188  cdlemg28b  41195  cdlemg28  41196  cdlemg33a  41198  cdlemg33b  41199  cdlemg33c  41200  cdlemg33d  41201  cdlemg33e  41202  cdlemg33  41203  cdlemg35  41205  cdlemg36  41206  cdlemg44a  41223  cdlemh  41309  cdlemi2  41311  cdlemj1  41313  tendocan  41316  cdlemk5a  41327  cdlemki  41333  cdlemkvcl  41334  cdlemk10  41335  cdlemksv2  41339  cdlemkole  41345  cdlemk14  41346  cdlemk15  41347  cdlemk16a  41348  cdlemk16  41349  cdlemk17  41350  cdlemk18  41360  cdlemk19  41361  cdlemkoatnle-2N  41367  cdlemk13-2N  41368  cdlemkole-2N  41369  cdlemk14-2N  41370  cdlemk15-2N  41371  cdlemk16-2N  41372  cdlemk17-2N  41373  cdlemk18-2N  41378  cdlemk19-2N  41379  cdlemk30  41386  cdlemk18-3N  41392  cdlemk23-3  41394  cdlemk25-3  41396  cdlemk27-3  41399  cdlemk37  41406  cdlemkfid1N  41413  cdlemkid1  41414  cdlemky  41418  cdlemk11ta  41421  cdlemk47  41441  cdlemk48  41442  cdlemk49  41443  cdlemk50  41444  cdlemk51  41445  cdlemk52  41446  cdlemk53a  41447  cdlemk54  41450  cdlemk39u1  41459  cdlemk19u1  41461  cdleml1N  41468  cdleml2N  41469  cdleml3N  41470  dia2dimlem6  41561  cdlemn2  41687  cdlemn2a  41688  cdlemn5pre  41692  cdlemn10  41698  cdlemn11c  41701  cdlemn11pre  41702  dihjustlem  41708  dihjust  41709  lclkrlem2y  42023  aks6d1c1  42601  relexpmulnn  44153  ormkglobd  47320  natglobalincr  47322  lincreslvec3  48973  iscnrm3llem1  49439  iscnrm3l  49441  swapffunc  49772  fucofunc  49849  amgmwlem  50292