Theorem simp21 1225

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp121  1324  simp221  1333  simp321  1342  omeulem1  8568  cofsmo  10254  axdc4lem  10440  0catg  17745  funcoppc  17933  funcres  17954  catcisolem  18168  1stfcl  18254  2ndfcl  18255  prfcl  18260  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  mulgdirlem  19172  ogrpsub  20208  ogrpaddlt  20209  ogrpsublt  20213  mdetunilem4  22753  mdetuni0  22759  mdetmul  22761  prdsxmetlem  24506  isosctrlem3  26966  isosctr  26967  amgmlem  27135  nosupbnd2lem1  27860  addsass  28179  f1otrg  29201  colinearalg  29241  ax5seglem6  29265  ax5seg  29269  axpasch  29272  axeuclidlem  29293  axeuclid  29294  uhgr2edg  29539  numclwlk1lem2  30702  rhmdvd  33625  bnj1128  35359  mclspps  36057  cgrtr  36465  cgrtr3  36467  ofscom  36480  segconeq  36483  ifscgr  36517  btwnxfr  36529  colinearxfr  36548  lineext  36549  brofs2  36550  brifs2  36551  fscgr  36553  linecgr  36554  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem6  36565  btwnconn1lem7  36566  seglecgr12im  36583  seglecgr12  36584  segletr  36587  broutsideof3  36599  outsideofeq  36603  lineunray  36620  lineelsb2  36621  linecom  36623  lshpkrlem5  39869  omlmod1i2N  40015  cvrnbtwn3  40031  cvrcmp  40038  cvrcmp2  40039  cvlexch2  40084  cvlexchb2  40086  cvlatexchb2  40090  cvlatexch2  40092  cvlatexch3  40093  cvlsupr7  40103  atnlej1  40134  atnlej2  40135  2llnneN  40164  cvratlem  40176  atcvrneN  40185  atcvrj1  40186  atlelt  40193  2atjm  40200  3noncolr2  40204  3noncolr1N  40205  3dimlem2  40214  3dim1  40222  3dim2  40223  1cvrat  40231  ps-1  40232  ps-2  40233  2atjlej  40234  hlatexch3N  40235  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem5  40242  3atlem6  40243  llnle  40273  2atm  40282  ps-2c  40283  lplni2  40292  lplnle  40295  lplnnle2at  40296  lplnri3N  40310  llncvrlpln2  40312  2atmat  40316  2llnm2N  40323  2llnm4  40325  2llnmeqat  40326  lvolnle3at  40337  4atlem0ae  40349  4atlem0be  40350  4atlem3b  40353  4atlem9  40358  4atlem10a  40359  4atlem10  40361  4atlem11a  40362  4atlem12a  40365  4at2  40369  2lplnm2N  40376  lneq2at  40533  2llnma1b  40541  2llnma1  40542  2llnma3r  40543  2llnma2  40544  2llnma2rN  40545  cdlema1N  40546  paddasslem2  40576  paddasslem15  40589  paddasslem16  40590  pmodlem1  40601  pmodlem2  40602  pmod2iN  40604  hlmod1i  40611  atmod1i1m  40613  atmod2i1  40616  atmod2i2  40617  atmod3i1  40619  atmod3i2  40620  atmod4i1  40621  atmod4i2  40622  llnexchb2lem  40623  llnexch2N  40625  dalawlem3  40628  dalawlem4  40629  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem9  40634  dalawlem11  40636  dalawlem12  40637  dalawlem13  40638  dalawlem15  40640  osumcllem9N  40719  pl42lem1N  40734  4atexlems  40807  4atex2  40832  4atex2-0bOLDN  40834  trlval4  40943  cdlemc5  40950  cdlemc6  40951  cdlemd2  40954  cdlemd4  40956  cdlemd6  40958  cdleme00a  40964  cdleme0e  40972  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme4  40993  cdleme4a  40994  cdleme5  40995  cdleme9  41008  cdleme16aN  41014  cdleme11c  41016  cdleme11e  41018  cdleme11g  41020  cdleme11h  41021  cdleme11j  41022  cdleme11k  41023  cdleme11l  41024  cdleme11  41025  cdleme12  41026  cdleme14  41028  cdleme15c  41031  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme0nex  41045  cdleme18a  41046  cdleme18c  41048  cdleme18d  41050  cdlemednpq  41054  cdlemednuN  41055  cdleme20zN  41056  cdleme20y  41057  cdleme19a  41058  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20aN  41064  cdleme20bN  41065  cdleme20c  41066  cdleme20d  41067  cdleme20f  41069  cdleme20g  41070  cdleme20i  41072  cdleme20j  41073  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21b  41081  cdleme21c  41082  cdleme21e  41086  cdleme21f  41087  cdleme22a  41095  cdleme22b  41096  cdleme22e  41099  cdleme22eALTN  41100  cdleme22f  41101  cdleme26eALTN  41116  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme27N  41124  cdleme28a  41125  cdleme28b  41126  cdleme30a  41133  cdleme43fsv1snlem  41175  cdlemefs31fv1  41179  cdlemefs45eN  41186  cdleme32b  41197  cdleme32c  41198  cdleme32d  41199  cdleme35h  41211  cdleme36a  41215  cdleme36m  41216  cdleme37m  41217  cdleme40m  41222  cdleme40n  41223  cdleme41sn3aw  41229  cdleme41sn4aw  41230  cdleme41fva11  41232  cdleme42k  41239  cdleme43cN  41246  cdleme43dN  41247  cdleme46f2g1  41249  cdlemeg47rv2  41265  cdlemeg46sfg  41275  cdlemeg46fjgN  41276  cdlemeg46rjgN  41277  cdlemeg46fjv  41278  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfv  41285  cdlemg4a  41363  cdlemg4d  41368  cdlemg4e  41369  cdlemg4f  41370  cdlemg4g  41371  cdlemg4  41372  cdlemg6d  41376  cdlemg6e  41377  cdlemg8b  41383  cdlemg8c  41384  cdlemg9a  41387  cdlemg9b  41388  cdlemg10a  41395  cdlemg10  41396  cdlemg12a  41398  cdlemg12b  41399  cdlemg12f  41403  cdlemg12g  41404  cdlemg12  41405  cdlemg17dN  41418  cdlemg17dALTN  41419  cdlemg17e  41420  cdlemg17f  41421  cdlemg17g  41422  cdlemg17h  41423  cdlemg17i  41424  cdlemg17pq  41427  cdlemg17iqN  41429  cdlemg17  41432  cdlemg18b  41434  cdlemg18c  41435  cdlemg19a  41438  cdlemg19  41439  cdlemg28a  41448  cdlemg27b  41451  cdlemg28b  41458  cdlemg28  41459  cdlemg33a  41461  cdlemg33b  41462  cdlemg33c  41463  cdlemg33d  41464  cdlemg33e  41465  cdlemg33  41466  cdlemg35  41468  cdlemg36  41469  cdlemg44a  41486  cdlemh  41572  cdlemi2  41574  cdlemj1  41576  tendocan  41579  cdlemk5a  41590  cdlemki  41596  cdlemkvcl  41597  cdlemk10  41598  cdlemksv2  41602  cdlemkole  41608  cdlemk14  41609  cdlemk15  41610  cdlemk16a  41611  cdlemk16  41612  cdlemk17  41613  cdlemk18  41623  cdlemk19  41624  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk30  41649  cdlemk18-3N  41655  cdlemk23-3  41657  cdlemk25-3  41659  cdlemk27-3  41662  cdlemk37  41669  cdlemkfid1N  41676  cdlemkid1  41677  cdlemky  41681  cdlemk11ta  41684  cdlemk47  41704  cdlemk48  41705  cdlemk49  41706  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemk53a  41710  cdlemk54  41713  cdlemk39u1  41722  cdlemk19u1  41724  cdleml1N  41731  cdleml2N  41732  cdleml3N  41733  dia2dimlem6  41824  cdlemn2  41950  cdlemn2a  41951  cdlemn5pre  41955  cdlemn10  41961  cdlemn11c  41964  cdlemn11pre  41965  dihjustlem  41971  dihjust  41972  lclkrlem2y  42286  aks6d1c1  42864  relexpmulnn  44418  ormkglobd  47574  natglobalincr  47576  lincreslvec3  49245  iscnrm3llem1  49710  iscnrm3l  49712  swapffunc  50043  fucofunc  50120  amgmwlem  50585