Theorem simp21 1087

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl21  1132  simpr21  1141  simp121  1186  simp221  1195  simp321  1204  omeulem1  7549  cofsmo  8974  axdc4lem  9160  0catg  16171  funcoppc  16358  funcres  16379  catcisolem  16579  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  mulgdirlem  17395  mdetunilem4  20240  mdetuni0  20246  mdetmul  20248  prdsxmetlem  21983  isosctrlem3  24350  isosctr  24351  amgmlem  24516  f1otrg  25551  colinearalg  25590  ax5seglem6  25614  ax5seg  25618  axpasch  25621  axeuclidlem  25642  axeuclid  25643  ogrpsub  29048  ogrpaddlt  29049  ogrpsublt  29053  rhmdvd  29152  bnj1128  30312  mclspps  30735  cgrtr  31269  cgrtr3  31271  ofscom  31284  segconeq  31287  ifscgr  31321  btwnxfr  31333  colinearxfr  31352  lineext  31353  brofs2  31354  brifs2  31355  fscgr  31357  linecgr  31358  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  seglecgr12im  31387  seglecgr12  31388  segletr  31391  broutsideof3  31403  outsideofeq  31407  lineunray  31424  lineelsb2  31425  linecom  31427  lshpkrlem5  33419  omlmod1i2N  33565  cvrnbtwn3  33581  cvrcmp  33588  cvrcmp2  33589  cvlexch2  33634  cvlexchb2  33636  cvlatexchb2  33640  cvlatexch2  33642  cvlatexch3  33643  cvlsupr7  33653  atnlej1  33683  atnlej2  33684  2llnneN  33713  cvratlem  33725  atcvrneN  33734  atcvrj1  33735  atlelt  33742  2atjm  33749  3noncolr2  33753  3noncolr1N  33754  3dimlem2  33763  3dim1  33771  3dim2  33772  1cvrat  33780  ps-1  33781  ps-2  33782  2atjlej  33783  hlatexch3N  33784  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem5  33791  3atlem6  33792  llnle  33822  2atm  33831  ps-2c  33832  lplni2  33841  lplnle  33844  lplnnle2at  33845  lplnri3N  33859  llncvrlpln2  33861  2atmat  33865  2llnm2N  33872  2llnm4  33874  2llnmeqat  33875  lvolnle3at  33886  4atlem0ae  33898  4atlem0be  33899  4atlem3b  33902  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem12a  33914  4at2  33918  2lplnm2N  33925  lneq2at  34082  2llnma1b  34090  2llnma1  34091  2llnma3r  34092  2llnma2  34093  2llnma2rN  34094  cdlema1N  34095  paddasslem2  34125  paddasslem15  34138  paddasslem16  34139  pmodlem1  34150  pmodlem2  34151  pmod2iN  34153  hlmod1i  34160  atmod1i1m  34162  atmod2i1  34165  atmod2i2  34166  atmod3i1  34168  atmod3i2  34169  atmod4i1  34170  atmod4i2  34171  llnexchb2lem  34172  llnexch2N  34174  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem13  34187  dalawlem15  34189  osumcllem9N  34268  pl42lem1N  34283  4atexlems  34356  4atex2  34381  4atex2-0bOLDN  34383  trlval4  34493  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdlemd4  34506  cdlemd6  34508  cdleme00a  34514  cdleme0e  34522  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme5  34545  cdleme9  34558  cdleme16aN  34564  cdleme11c  34566  cdleme11e  34568  cdleme11g  34570  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme11l  34574  cdleme11  34575  cdleme12  34576  cdleme14  34578  cdleme15c  34581  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme0nex  34595  cdleme18a  34596  cdleme18c  34598  cdleme18d  34600  cdlemednpq  34604  cdlemednuN  34605  cdleme20zN  34606  cdleme20y  34607  cdleme20yOLD  34608  cdleme19a  34609  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20aN  34615  cdleme20bN  34616  cdleme20c  34617  cdleme20d  34618  cdleme20f  34620  cdleme20g  34621  cdleme20i  34623  cdleme20j  34624  cdleme20l1  34626  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21b  34632  cdleme21c  34633  cdleme21e  34637  cdleme21f  34638  cdleme22a  34646  cdleme22b  34647  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme26eALTN  34667  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme27N  34675  cdleme28a  34676  cdleme28b  34677  cdleme30a  34684  cdleme43fsv1snlem  34726  cdlemefs31fv1  34730  cdlemefs45eN  34737  cdleme32b  34748  cdleme32c  34749  cdleme32d  34750  cdleme35h  34762  cdleme36a  34766  cdleme36m  34767  cdleme37m  34768  cdleme40m  34773  cdleme40n  34774  cdleme41sn3aw  34780  cdleme41sn4aw  34781  cdleme41fva11  34783  cdleme42k  34790  cdleme43cN  34797  cdleme43dN  34798  cdleme46f2g1  34800  cdlemeg47rv2  34816  cdlemeg46sfg  34826  cdlemeg46fjgN  34827  cdlemeg46rjgN  34828  cdlemeg46fjv  34829  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdlemg4a  34914  cdlemg4d  34919  cdlemg4e  34920  cdlemg4f  34921  cdlemg4g  34922  cdlemg4  34923  cdlemg6d  34927  cdlemg6e  34928  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9b  34939  cdlemg10a  34946  cdlemg10  34947  cdlemg12a  34949  cdlemg12b  34950  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg17dN  34969  cdlemg17dALTN  34970  cdlemg17e  34971  cdlemg17f  34972  cdlemg17g  34973  cdlemg17h  34974  cdlemg17i  34975  cdlemg17pq  34978  cdlemg17iqN  34980  cdlemg17  34983  cdlemg18b  34985  cdlemg18c  34986  cdlemg19a  34989  cdlemg19  34990  cdlemg28a  34999  cdlemg27b  35002  cdlemg28b  35009  cdlemg28  35010  cdlemg33a  35012  cdlemg33b  35013  cdlemg33c  35014  cdlemg33d  35015  cdlemg33e  35016  cdlemg33  35017  cdlemg35  35019  cdlemg36  35020  cdlemg44a  35037  cdlemh  35123  cdlemi2  35125  cdlemj1  35127  tendocan  35130  cdlemk5a  35141  cdlemki  35147  cdlemkvcl  35148  cdlemk10  35149  cdlemksv2  35153  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk16a  35162  cdlemk16  35163  cdlemk17  35164  cdlemk18  35174  cdlemk19  35175  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk30  35200  cdlemk18-3N  35206  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk27-3  35213  cdlemk37  35220  cdlemkfid1N  35227  cdlemkid1  35228  cdlemky  35232  cdlemk11ta  35235  cdlemk47  35255  cdlemk48  35256  cdlemk49  35257  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk53a  35261  cdlemk54  35264  cdlemk39u1  35273  cdlemk19u1  35275  cdleml1N  35282  cdleml2N  35283  cdleml3N  35284  dia2dimlem6  35376  cdlemn2  35502  cdlemn2a  35503  cdlemn5pre  35507  cdlemn10  35513  cdlemn11c  35516  cdlemn11pre  35517  dihjustlem  35523  dihjust  35524  lclkrlem2y  35838  relexpmulnn  37020  uhgr2edg  40435  lincreslvec3  42065  amgmwlem  42357