Theorem simp21 1205

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 1135	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1133	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  1304  simp221  1313  simp321  1322  omeulem1  8618  cofsmo  10306  axdc4lem  10492  0catg  17732  funcoppc  17925  funcres  17946  catcisolem  18163  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  mulgdirlem  19135  mdetunilem4  22636  mdetuni0  22642  mdetmul  22644  prdsxmetlem  24393  isosctrlem3  26877  isosctr  26878  amgmlem  27047  nosupbnd2lem1  27774  addsass  28052  f1otrg  28893  colinearalg  28939  ax5seglem6  28963  ax5seg  28967  axpasch  28970  axeuclidlem  28991  axeuclid  28992  uhgr2edg  29239  numclwlk1lem2  30398  ogrpsub  33075  ogrpaddlt  33076  ogrpsublt  33080  rhmdvd  33327  bnj1128  34982  mclspps  35568  cgrtr  35973  cgrtr3  35975  ofscom  35988  segconeq  35991  ifscgr  36025  btwnxfr  36037  colinearxfr  36056  lineext  36057  brofs2  36058  brifs2  36059  fscgr  36061  linecgr  36062  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem7  36074  seglecgr12im  36091  seglecgr12  36092  segletr  36095  broutsideof3  36107  outsideofeq  36111  lineunray  36128  lineelsb2  36129  linecom  36131  lshpkrlem5  39095  omlmod1i2N  39241  cvrnbtwn3  39257  cvrcmp  39264  cvrcmp2  39265  cvlexch2  39310  cvlexchb2  39312  cvlatexchb2  39316  cvlatexch2  39318  cvlatexch3  39319  cvlsupr7  39329  atnlej1  39361  atnlej2  39362  2llnneN  39391  cvratlem  39403  atcvrneN  39412  atcvrj1  39413  atlelt  39420  2atjm  39427  3noncolr2  39431  3noncolr1N  39432  3dimlem2  39441  3dim1  39449  3dim2  39450  1cvrat  39458  ps-1  39459  ps-2  39460  2atjlej  39461  hlatexch3N  39462  ps-2b  39464  3atlem1  39465  3atlem2  39466  3atlem5  39469  3atlem6  39470  llnle  39500  2atm  39509  ps-2c  39510  lplni2  39519  lplnle  39522  lplnnle2at  39523  lplnri3N  39537  llncvrlpln2  39539  2atmat  39543  2llnm2N  39550  2llnm4  39552  2llnmeqat  39553  lvolnle3at  39564  4atlem0ae  39576  4atlem0be  39577  4atlem3b  39580  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem12a  39592  4at2  39596  2lplnm2N  39603  lneq2at  39760  2llnma1b  39768  2llnma1  39769  2llnma3r  39770  2llnma2  39771  2llnma2rN  39772  cdlema1N  39773  paddasslem2  39803  paddasslem15  39816  paddasslem16  39817  pmodlem1  39828  pmodlem2  39829  pmod2iN  39831  hlmod1i  39838  atmod1i1m  39840  atmod2i1  39843  atmod2i2  39844  atmod3i1  39846  atmod3i2  39847  atmod4i1  39848  atmod4i2  39849  llnexchb2lem  39850  llnexch2N  39852  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem13  39865  dalawlem15  39867  osumcllem9N  39946  pl42lem1N  39961  4atexlems  40034  4atex2  40059  4atex2-0bOLDN  40061  trlval4  40170  cdlemc5  40177  cdlemc6  40178  cdlemd2  40181  cdlemd4  40183  cdlemd6  40185  cdleme00a  40191  cdleme0e  40199  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme4a  40221  cdleme5  40222  cdleme9  40235  cdleme16aN  40241  cdleme11c  40243  cdleme11e  40245  cdleme11g  40247  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme11l  40251  cdleme11  40252  cdleme12  40253  cdleme14  40255  cdleme15c  40258  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme0nex  40272  cdleme18a  40273  cdleme18c  40275  cdleme18d  40277  cdlemednpq  40281  cdlemednuN  40282  cdleme20zN  40283  cdleme20y  40284  cdleme19a  40285  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20aN  40291  cdleme20bN  40292  cdleme20c  40293  cdleme20d  40294  cdleme20f  40296  cdleme20g  40297  cdleme20i  40299  cdleme20j  40300  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21b  40308  cdleme21c  40309  cdleme21e  40313  cdleme21f  40314  cdleme22a  40322  cdleme22b  40323  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme26eALTN  40343  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme30a  40360  cdleme43fsv1snlem  40402  cdlemefs31fv1  40406  cdlemefs45eN  40413  cdleme32b  40424  cdleme32c  40425  cdleme32d  40426  cdleme35h  40438  cdleme36a  40442  cdleme36m  40443  cdleme37m  40444  cdleme40m  40449  cdleme40n  40450  cdleme41sn3aw  40456  cdleme41sn4aw  40457  cdleme41fva11  40459  cdleme42k  40466  cdleme43cN  40473  cdleme43dN  40474  cdleme46f2g1  40476  cdlemeg47rv2  40492  cdlemeg46sfg  40502  cdlemeg46fjgN  40503  cdlemeg46rjgN  40504  cdlemeg46fjv  40505  cdlemeg46frv  40507  cdlemeg46vrg  40509  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdlemg4a  40590  cdlemg4d  40595  cdlemg4e  40596  cdlemg4f  40597  cdlemg4g  40598  cdlemg4  40599  cdlemg6d  40603  cdlemg6e  40604  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg9b  40615  cdlemg10a  40622  cdlemg10  40623  cdlemg12a  40625  cdlemg12b  40626  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg17dN  40645  cdlemg17dALTN  40646  cdlemg17e  40647  cdlemg17f  40648  cdlemg17g  40649  cdlemg17h  40650  cdlemg17i  40651  cdlemg17pq  40654  cdlemg17iqN  40656  cdlemg17  40659  cdlemg18b  40661  cdlemg18c  40662  cdlemg19a  40665  cdlemg19  40666  cdlemg28a  40675  cdlemg27b  40678  cdlemg28b  40685  cdlemg28  40686  cdlemg33a  40688  cdlemg33b  40689  cdlemg33c  40690  cdlemg33d  40691  cdlemg33e  40692  cdlemg33  40693  cdlemg35  40695  cdlemg36  40696  cdlemg44a  40713  cdlemh  40799  cdlemi2  40801  cdlemj1  40803  tendocan  40806  cdlemk5a  40817  cdlemki  40823  cdlemkvcl  40824  cdlemk10  40825  cdlemksv2  40829  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk16a  40838  cdlemk16  40839  cdlemk17  40840  cdlemk18  40850  cdlemk19  40851  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk30  40876  cdlemk18-3N  40882  cdlemk23-3  40884  cdlemk25-3  40886  cdlemk27-3  40889  cdlemk37  40896  cdlemkfid1N  40903  cdlemkid1  40904  cdlemky  40908  cdlemk11ta  40911  cdlemk47  40931  cdlemk48  40932  cdlemk49  40933  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdlemk54  40940  cdlemk39u1  40949  cdlemk19u1  40951  cdleml1N  40958  cdleml2N  40959  cdleml3N  40960  dia2dimlem6  41051  cdlemn2  41177  cdlemn2a  41178  cdlemn5pre  41182  cdlemn10  41188  cdlemn11c  41191  cdlemn11pre  41192  dihjustlem  41198  dihjust  41199  lclkrlem2y  41513  aks6d1c1  42097  relexpmulnn  43698  natglobalincr  46830  lincreslvec3  48327  iscnrm3llem1  48745  iscnrm3l  48747  amgmwlem  49032