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  8507  cofsmo  10182  axdc4lem  10368  0catg  17612  funcoppc  17800  funcres  17821  catcisolem  18035  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  mulgdirlem  19002  ogrpsub  20034  ogrpaddlt  20035  ogrpsublt  20039  mdetunilem4  22518  mdetuni0  22524  mdetmul  22526  prdsxmetlem  24272  isosctrlem3  26746  isosctr  26747  amgmlem  26916  nosupbnd2lem1  27643  addsass  27935  f1otrg  28834  colinearalg  28873  ax5seglem6  28897  ax5seg  28901  axpasch  28904  axeuclidlem  28925  axeuclid  28926  uhgr2edg  29171  numclwlk1lem2  30332  rhmdvd  33275  bnj1128  34959  mclspps  35559  cgrtr  35968  cgrtr3  35970  ofscom  35983  segconeq  35986  ifscgr  36020  btwnxfr  36032  colinearxfr  36051  lineext  36052  brofs2  36053  brifs2  36054  fscgr  36056  linecgr  36057  btwnconn1lem1  36063  btwnconn1lem2  36064  btwnconn1lem3  36065  btwnconn1lem4  36066  btwnconn1lem5  36067  btwnconn1lem6  36068  btwnconn1lem7  36069  seglecgr12im  36086  seglecgr12  36087  segletr  36090  broutsideof3  36102  outsideofeq  36106  lineunray  36123  lineelsb2  36124  linecom  36126  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  42092  relexpmulnn  43685  ormkglobd  46860  natglobalincr  46862  lincreslvec3  48471  iscnrm3llem1  48937  iscnrm3l  48939  swapffunc  49271  fucofunc  49348  amgmwlem  49791