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  8546  cofsmo  10222  axdc4lem  10408  0catg  17649  funcoppc  17837  funcres  17858  catcisolem  18072  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  mulgdirlem  19037  mdetunilem4  22502  mdetuni0  22508  mdetmul  22510  prdsxmetlem  24256  isosctrlem3  26730  isosctr  26731  amgmlem  26900  nosupbnd2lem1  27627  addsass  27912  f1otrg  28798  colinearalg  28837  ax5seglem6  28861  ax5seg  28865  axpasch  28868  axeuclidlem  28889  axeuclid  28890  uhgr2edg  29135  numclwlk1lem2  30299  ogrpsub  33030  ogrpaddlt  33031  ogrpsublt  33035  rhmdvd  33296  bnj1128  34980  mclspps  35571  cgrtr  35980  cgrtr3  35982  ofscom  35995  segconeq  35998  ifscgr  36032  btwnxfr  36044  colinearxfr  36063  lineext  36064  brofs2  36065  brifs2  36066  fscgr  36068  linecgr  36069  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  seglecgr12im  36098  seglecgr12  36099  segletr  36102  broutsideof3  36114  outsideofeq  36118  lineunray  36135  lineelsb2  36136  linecom  36138  lshpkrlem5  39107  omlmod1i2N  39253  cvrnbtwn3  39269  cvrcmp  39276  cvrcmp2  39277  cvlexch2  39322  cvlexchb2  39324  cvlatexchb2  39328  cvlatexch2  39330  cvlatexch3  39331  cvlsupr7  39341  atnlej1  39373  atnlej2  39374  2llnneN  39403  cvratlem  39415  atcvrneN  39424  atcvrj1  39425  atlelt  39432  2atjm  39439  3noncolr2  39443  3noncolr1N  39444  3dimlem2  39453  3dim1  39461  3dim2  39462  1cvrat  39470  ps-1  39471  ps-2  39472  2atjlej  39473  hlatexch3N  39474  ps-2b  39476  3atlem1  39477  3atlem2  39478  3atlem5  39481  3atlem6  39482  llnle  39512  2atm  39521  ps-2c  39522  lplni2  39531  lplnle  39534  lplnnle2at  39535  lplnri3N  39549  llncvrlpln2  39551  2atmat  39555  2llnm2N  39562  2llnm4  39564  2llnmeqat  39565  lvolnle3at  39576  4atlem0ae  39588  4atlem0be  39589  4atlem3b  39592  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem12a  39604  4at2  39608  2lplnm2N  39615  lneq2at  39772  2llnma1b  39780  2llnma1  39781  2llnma3r  39782  2llnma2  39783  2llnma2rN  39784  cdlema1N  39785  paddasslem2  39815  paddasslem15  39828  paddasslem16  39829  pmodlem1  39840  pmodlem2  39841  pmod2iN  39843  hlmod1i  39850  atmod1i1m  39852  atmod2i1  39855  atmod2i2  39856  atmod3i1  39858  atmod3i2  39859  atmod4i1  39860  atmod4i2  39861  llnexchb2lem  39862  llnexch2N  39864  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem13  39877  dalawlem15  39879  osumcllem9N  39958  pl42lem1N  39973  4atexlems  40046  4atex2  40071  4atex2-0bOLDN  40073  trlval4  40182  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdlemd4  40195  cdlemd6  40197  cdleme00a  40203  cdleme0e  40211  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme5  40234  cdleme9  40247  cdleme16aN  40253  cdleme11c  40255  cdleme11e  40257  cdleme11g  40259  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme11l  40263  cdleme11  40264  cdleme12  40265  cdleme14  40267  cdleme15c  40270  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme0nex  40284  cdleme18a  40285  cdleme18c  40287  cdleme18d  40289  cdlemednpq  40293  cdlemednuN  40294  cdleme20zN  40295  cdleme20y  40296  cdleme19a  40297  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20aN  40303  cdleme20bN  40304  cdleme20c  40305  cdleme20d  40306  cdleme20f  40308  cdleme20g  40309  cdleme20i  40311  cdleme20j  40312  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21b  40320  cdleme21c  40321  cdleme21e  40325  cdleme21f  40326  cdleme22a  40334  cdleme22b  40335  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme26eALTN  40355  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme30a  40372  cdleme43fsv1snlem  40414  cdlemefs31fv1  40418  cdlemefs45eN  40425  cdleme32b  40436  cdleme32c  40437  cdleme32d  40438  cdleme35h  40450  cdleme36a  40454  cdleme36m  40455  cdleme37m  40456  cdleme40m  40461  cdleme40n  40462  cdleme41sn3aw  40468  cdleme41sn4aw  40469  cdleme41fva11  40471  cdleme42k  40478  cdleme43cN  40485  cdleme43dN  40486  cdleme46f2g1  40488  cdlemeg47rv2  40504  cdlemeg46sfg  40514  cdlemeg46fjgN  40515  cdlemeg46rjgN  40516  cdlemeg46fjv  40517  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdlemg4a  40602  cdlemg4d  40607  cdlemg4e  40608  cdlemg4f  40609  cdlemg4g  40610  cdlemg4  40611  cdlemg6d  40615  cdlemg6e  40616  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9b  40627  cdlemg10a  40634  cdlemg10  40635  cdlemg12a  40637  cdlemg12b  40638  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg17dN  40657  cdlemg17dALTN  40658  cdlemg17e  40659  cdlemg17f  40660  cdlemg17g  40661  cdlemg17h  40662  cdlemg17i  40663  cdlemg17pq  40666  cdlemg17iqN  40668  cdlemg17  40671  cdlemg18b  40673  cdlemg18c  40674  cdlemg19a  40677  cdlemg19  40678  cdlemg28a  40687  cdlemg27b  40690  cdlemg28b  40697  cdlemg28  40698  cdlemg33a  40700  cdlemg33b  40701  cdlemg33c  40702  cdlemg33d  40703  cdlemg33e  40704  cdlemg33  40705  cdlemg35  40707  cdlemg36  40708  cdlemg44a  40725  cdlemh  40811  cdlemi2  40813  cdlemj1  40815  tendocan  40818  cdlemk5a  40829  cdlemki  40835  cdlemkvcl  40836  cdlemk10  40837  cdlemksv2  40841  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk16a  40850  cdlemk16  40851  cdlemk17  40852  cdlemk18  40862  cdlemk19  40863  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk30  40888  cdlemk18-3N  40894  cdlemk23-3  40896  cdlemk25-3  40898  cdlemk27-3  40901  cdlemk37  40908  cdlemkfid1N  40915  cdlemkid1  40916  cdlemky  40920  cdlemk11ta  40923  cdlemk47  40943  cdlemk48  40944  cdlemk49  40945  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk53a  40949  cdlemk54  40952  cdlemk39u1  40961  cdlemk19u1  40963  cdleml1N  40970  cdleml2N  40971  cdleml3N  40972  dia2dimlem6  41063  cdlemn2  41189  cdlemn2a  41190  cdlemn5pre  41194  cdlemn10  41200  cdlemn11c  41203  cdlemn11pre  41204  dihjustlem  41210  dihjust  41211  lclkrlem2y  41525  aks6d1c1  42104  relexpmulnn  43698  ormkglobd  46873  natglobalincr  46875  lincreslvec3  48471  iscnrm3llem1  48937  iscnrm3l  48939  swapffunc  49271  fucofunc  49348  amgmwlem  49791