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  8549  cofsmo  10229  axdc4lem  10415  0catg  17656  funcoppc  17844  funcres  17865  catcisolem  18079  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  mulgdirlem  19044  mdetunilem4  22509  mdetuni0  22515  mdetmul  22517  prdsxmetlem  24263  isosctrlem3  26737  isosctr  26738  amgmlem  26907  nosupbnd2lem1  27634  addsass  27919  f1otrg  28805  colinearalg  28844  ax5seglem6  28868  ax5seg  28872  axpasch  28875  axeuclidlem  28896  axeuclid  28897  uhgr2edg  29142  numclwlk1lem2  30306  ogrpsub  33037  ogrpaddlt  33038  ogrpsublt  33042  rhmdvd  33303  bnj1128  34987  mclspps  35578  cgrtr  35987  cgrtr3  35989  ofscom  36002  segconeq  36005  ifscgr  36039  btwnxfr  36051  colinearxfr  36070  lineext  36071  brofs2  36072  brifs2  36073  fscgr  36075  linecgr  36076  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  seglecgr12im  36105  seglecgr12  36106  segletr  36109  broutsideof3  36121  outsideofeq  36125  lineunray  36142  lineelsb2  36143  linecom  36145  lshpkrlem5  39114  omlmod1i2N  39260  cvrnbtwn3  39276  cvrcmp  39283  cvrcmp2  39284  cvlexch2  39329  cvlexchb2  39331  cvlatexchb2  39335  cvlatexch2  39337  cvlatexch3  39338  cvlsupr7  39348  atnlej1  39380  atnlej2  39381  2llnneN  39410  cvratlem  39422  atcvrneN  39431  atcvrj1  39432  atlelt  39439  2atjm  39446  3noncolr2  39450  3noncolr1N  39451  3dimlem2  39460  3dim1  39468  3dim2  39469  1cvrat  39477  ps-1  39478  ps-2  39479  2atjlej  39480  hlatexch3N  39481  ps-2b  39483  3atlem1  39484  3atlem2  39485  3atlem5  39488  3atlem6  39489  llnle  39519  2atm  39528  ps-2c  39529  lplni2  39538  lplnle  39541  lplnnle2at  39542  lplnri3N  39556  llncvrlpln2  39558  2atmat  39562  2llnm2N  39569  2llnm4  39571  2llnmeqat  39572  lvolnle3at  39583  4atlem0ae  39595  4atlem0be  39596  4atlem3b  39599  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem12a  39611  4at2  39615  2lplnm2N  39622  lneq2at  39779  2llnma1b  39787  2llnma1  39788  2llnma3r  39789  2llnma2  39790  2llnma2rN  39791  cdlema1N  39792  paddasslem2  39822  paddasslem15  39835  paddasslem16  39836  pmodlem1  39847  pmodlem2  39848  pmod2iN  39850  hlmod1i  39857  atmod1i1m  39859  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  atmod3i2  39866  atmod4i1  39867  atmod4i2  39868  llnexchb2lem  39869  llnexch2N  39871  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem13  39884  dalawlem15  39886  osumcllem9N  39965  pl42lem1N  39980  4atexlems  40053  4atex2  40078  4atex2-0bOLDN  40080  trlval4  40189  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdlemd4  40202  cdlemd6  40204  cdleme00a  40210  cdleme0e  40218  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme4a  40240  cdleme5  40241  cdleme9  40254  cdleme16aN  40260  cdleme11c  40262  cdleme11e  40264  cdleme11g  40266  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme11l  40270  cdleme11  40271  cdleme12  40272  cdleme14  40274  cdleme15c  40277  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme0nex  40291  cdleme18a  40292  cdleme18c  40294  cdleme18d  40296  cdlemednpq  40300  cdlemednuN  40301  cdleme20zN  40302  cdleme20y  40303  cdleme19a  40304  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20aN  40310  cdleme20bN  40311  cdleme20c  40312  cdleme20d  40313  cdleme20f  40315  cdleme20g  40316  cdleme20i  40318  cdleme20j  40319  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21b  40327  cdleme21c  40328  cdleme21e  40332  cdleme21f  40333  cdleme22a  40341  cdleme22b  40342  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme26eALTN  40362  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme30a  40379  cdleme43fsv1snlem  40421  cdlemefs31fv1  40425  cdlemefs45eN  40432  cdleme32b  40443  cdleme32c  40444  cdleme32d  40445  cdleme35h  40457  cdleme36a  40461  cdleme36m  40462  cdleme37m  40463  cdleme40m  40468  cdleme40n  40469  cdleme41sn3aw  40475  cdleme41sn4aw  40476  cdleme41fva11  40478  cdleme42k  40485  cdleme43cN  40492  cdleme43dN  40493  cdleme46f2g1  40495  cdlemeg47rv2  40511  cdlemeg46sfg  40521  cdlemeg46fjgN  40522  cdlemeg46rjgN  40523  cdlemeg46fjv  40524  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdlemg4a  40609  cdlemg4d  40614  cdlemg4e  40615  cdlemg4f  40616  cdlemg4g  40617  cdlemg4  40618  cdlemg6d  40622  cdlemg6e  40623  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg10a  40641  cdlemg10  40642  cdlemg12a  40644  cdlemg12b  40645  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg17dN  40664  cdlemg17dALTN  40665  cdlemg17e  40666  cdlemg17f  40667  cdlemg17g  40668  cdlemg17h  40669  cdlemg17i  40670  cdlemg17pq  40673  cdlemg17iqN  40675  cdlemg17  40678  cdlemg18b  40680  cdlemg18c  40681  cdlemg19a  40684  cdlemg19  40685  cdlemg28a  40694  cdlemg27b  40697  cdlemg28b  40704  cdlemg28  40705  cdlemg33a  40707  cdlemg33b  40708  cdlemg33c  40709  cdlemg33d  40710  cdlemg33e  40711  cdlemg33  40712  cdlemg35  40714  cdlemg36  40715  cdlemg44a  40732  cdlemh  40818  cdlemi2  40820  cdlemj1  40822  tendocan  40825  cdlemk5a  40836  cdlemki  40842  cdlemkvcl  40843  cdlemk10  40844  cdlemksv2  40848  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk16a  40857  cdlemk16  40858  cdlemk17  40859  cdlemk18  40869  cdlemk19  40870  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk30  40895  cdlemk18-3N  40901  cdlemk23-3  40903  cdlemk25-3  40905  cdlemk27-3  40908  cdlemk37  40915  cdlemkfid1N  40922  cdlemkid1  40923  cdlemky  40927  cdlemk11ta  40930  cdlemk47  40950  cdlemk48  40951  cdlemk49  40952  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk53a  40956  cdlemk54  40959  cdlemk39u1  40968  cdlemk19u1  40970  cdleml1N  40977  cdleml2N  40978  cdleml3N  40979  dia2dimlem6  41070  cdlemn2  41196  cdlemn2a  41197  cdlemn5pre  41201  cdlemn10  41207  cdlemn11c  41210  cdlemn11pre  41211  dihjustlem  41217  dihjust  41218  lclkrlem2y  41532  aks6d1c1  42111  relexpmulnn  43705  ormkglobd  46880  natglobalincr  46882  lincreslvec3  48475  iscnrm3llem1  48941  iscnrm3l  48943  swapffunc  49275  fucofunc  49352  amgmwlem  49795