Theorem simp21 1219

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp121  1318  simp221  1327  simp321  1336  omeulem1  8545  cofsmo  10220  axdc4lem  10406  0catg  17711  funcoppc  17899  funcres  17920  catcisolem  18134  1stfcl  18220  2ndfcl  18221  prfcl  18226  evlfcl  18245  curf1cl  18251  curfcl  18255  hofcl  18282  mulgdirlem  19138  ogrpsub  20168  ogrpaddlt  20169  ogrpsublt  20173  mdetunilem4  22663  mdetuni0  22669  mdetmul  22671  prdsxmetlem  24416  isosctrlem3  26873  isosctr  26874  amgmlem  27042  nosupbnd2lem1  27767  addsass  28086  f1otrg  29028  colinearalg  29068  ax5seglem6  29092  ax5seg  29096  axpasch  29099  axeuclidlem  29120  axeuclid  29121  uhgr2edg  29366  numclwlk1lem2  30529  rhmdvd  33471  bnj1128  35246  mclspps  35895  cgrtr  36303  cgrtr3  36305  ofscom  36318  segconeq  36321  ifscgr  36355  btwnxfr  36367  colinearxfr  36386  lineext  36387  brofs2  36388  brifs2  36389  fscgr  36391  linecgr  36392  btwnconn1lem1  36398  btwnconn1lem2  36399  btwnconn1lem3  36400  btwnconn1lem4  36401  btwnconn1lem5  36402  btwnconn1lem6  36403  btwnconn1lem7  36404  seglecgr12im  36421  seglecgr12  36422  segletr  36425  broutsideof3  36437  outsideofeq  36441  lineunray  36458  lineelsb2  36459  linecom  36461  lshpkrlem5  39699  omlmod1i2N  39845  cvrnbtwn3  39861  cvrcmp  39868  cvrcmp2  39869  cvlexch2  39914  cvlexchb2  39916  cvlatexchb2  39920  cvlatexch2  39922  cvlatexch3  39923  cvlsupr7  39933  atnlej1  39964  atnlej2  39965  2llnneN  39994  cvratlem  40006  atcvrneN  40015  atcvrj1  40016  atlelt  40023  2atjm  40030  3noncolr2  40034  3noncolr1N  40035  3dimlem2  40044  3dim1  40052  3dim2  40053  1cvrat  40061  ps-1  40062  ps-2  40063  2atjlej  40064  hlatexch3N  40065  ps-2b  40067  3atlem1  40068  3atlem2  40069  3atlem5  40072  3atlem6  40073  llnle  40103  2atm  40112  ps-2c  40113  lplni2  40122  lplnle  40125  lplnnle2at  40126  lplnri3N  40140  llncvrlpln2  40142  2atmat  40146  2llnm2N  40153  2llnm4  40155  2llnmeqat  40156  lvolnle3at  40167  4atlem0ae  40179  4atlem0be  40180  4atlem3b  40183  4atlem9  40188  4atlem10a  40189  4atlem10  40191  4atlem11a  40192  4atlem12a  40195  4at2  40199  2lplnm2N  40206  lneq2at  40363  2llnma1b  40371  2llnma1  40372  2llnma3r  40373  2llnma2  40374  2llnma2rN  40375  cdlema1N  40376  paddasslem2  40406  paddasslem15  40419  paddasslem16  40420  pmodlem1  40431  pmodlem2  40432  pmod2iN  40434  hlmod1i  40441  atmod1i1m  40443  atmod2i1  40446  atmod2i2  40447  atmod3i1  40449  atmod3i2  40450  atmod4i1  40451  atmod4i2  40452  llnexchb2lem  40453  llnexch2N  40455  dalawlem3  40458  dalawlem4  40459  dalawlem5  40460  dalawlem6  40461  dalawlem7  40462  dalawlem8  40463  dalawlem9  40464  dalawlem11  40466  dalawlem12  40467  dalawlem13  40468  dalawlem15  40470  osumcllem9N  40549  pl42lem1N  40564  4atexlems  40637  4atex2  40662  4atex2-0bOLDN  40664  trlval4  40773  cdlemc5  40780  cdlemc6  40781  cdlemd2  40784  cdlemd4  40786  cdlemd6  40788  cdleme00a  40794  cdleme0e  40802  cdleme3g  40819  cdleme3h  40820  cdleme3  40822  cdleme4  40823  cdleme4a  40824  cdleme5  40825  cdleme9  40838  cdleme16aN  40844  cdleme11c  40846  cdleme11e  40848  cdleme11g  40850  cdleme11h  40851  cdleme11j  40852  cdleme11k  40853  cdleme11l  40854  cdleme11  40855  cdleme12  40856  cdleme14  40858  cdleme15c  40861  cdleme16b  40864  cdleme16c  40865  cdleme16d  40866  cdleme16e  40867  cdleme16f  40868  cdleme0nex  40875  cdleme18a  40876  cdleme18c  40878  cdleme18d  40880  cdlemednpq  40884  cdlemednuN  40885  cdleme20zN  40886  cdleme20y  40887  cdleme19a  40888  cdleme19b  40889  cdleme19d  40891  cdleme19e  40892  cdleme20aN  40894  cdleme20bN  40895  cdleme20c  40896  cdleme20d  40897  cdleme20f  40899  cdleme20g  40900  cdleme20i  40902  cdleme20j  40903  cdleme20l1  40905  cdleme20l2  40906  cdleme20l  40907  cdleme20m  40908  cdleme21b  40911  cdleme21c  40912  cdleme21e  40916  cdleme21f  40917  cdleme22a  40925  cdleme22b  40926  cdleme22e  40929  cdleme22eALTN  40930  cdleme22f  40931  cdleme26eALTN  40946  cdleme26fALTN  40947  cdleme26f  40948  cdleme26f2ALTN  40949  cdleme26f2  40950  cdleme27N  40954  cdleme28a  40955  cdleme28b  40956  cdleme30a  40963  cdleme43fsv1snlem  41005  cdlemefs31fv1  41009  cdlemefs45eN  41016  cdleme32b  41027  cdleme32c  41028  cdleme32d  41029  cdleme35h  41041  cdleme36a  41045  cdleme36m  41046  cdleme37m  41047  cdleme40m  41052  cdleme40n  41053  cdleme41sn3aw  41059  cdleme41sn4aw  41060  cdleme41fva11  41062  cdleme42k  41069  cdleme43cN  41076  cdleme43dN  41077  cdleme46f2g1  41079  cdlemeg47rv2  41095  cdlemeg46sfg  41105  cdlemeg46fjgN  41106  cdlemeg46rjgN  41107  cdlemeg46fjv  41108  cdlemeg46frv  41110  cdlemeg46vrg  41112  cdlemeg46rgv  41113  cdlemeg46req  41114  cdlemeg46gfv  41115  cdlemg4a  41193  cdlemg4d  41198  cdlemg4e  41199  cdlemg4f  41200  cdlemg4g  41201  cdlemg4  41202  cdlemg6d  41206  cdlemg6e  41207  cdlemg8b  41213  cdlemg8c  41214  cdlemg9a  41217  cdlemg9b  41218  cdlemg10a  41225  cdlemg10  41226  cdlemg12a  41228  cdlemg12b  41229  cdlemg12f  41233  cdlemg12g  41234  cdlemg12  41235  cdlemg17dN  41248  cdlemg17dALTN  41249  cdlemg17e  41250  cdlemg17f  41251  cdlemg17g  41252  cdlemg17h  41253  cdlemg17i  41254  cdlemg17pq  41257  cdlemg17iqN  41259  cdlemg17  41262  cdlemg18b  41264  cdlemg18c  41265  cdlemg19a  41268  cdlemg19  41269  cdlemg28a  41278  cdlemg27b  41281  cdlemg28b  41288  cdlemg28  41289  cdlemg33a  41291  cdlemg33b  41292  cdlemg33c  41293  cdlemg33d  41294  cdlemg33e  41295  cdlemg33  41296  cdlemg35  41298  cdlemg36  41299  cdlemg44a  41316  cdlemh  41402  cdlemi2  41404  cdlemj1  41406  tendocan  41409  cdlemk5a  41420  cdlemki  41426  cdlemkvcl  41427  cdlemk10  41428  cdlemksv2  41432  cdlemkole  41438  cdlemk14  41439  cdlemk15  41440  cdlemk16a  41441  cdlemk16  41442  cdlemk17  41443  cdlemk18  41453  cdlemk19  41454  cdlemkoatnle-2N  41460  cdlemk13-2N  41461  cdlemkole-2N  41462  cdlemk14-2N  41463  cdlemk15-2N  41464  cdlemk16-2N  41465  cdlemk17-2N  41466  cdlemk18-2N  41471  cdlemk19-2N  41472  cdlemk30  41479  cdlemk18-3N  41485  cdlemk23-3  41487  cdlemk25-3  41489  cdlemk27-3  41492  cdlemk37  41499  cdlemkfid1N  41506  cdlemkid1  41507  cdlemky  41511  cdlemk11ta  41514  cdlemk47  41534  cdlemk48  41535  cdlemk49  41536  cdlemk50  41537  cdlemk51  41538  cdlemk52  41539  cdlemk53a  41540  cdlemk54  41543  cdlemk39u1  41552  cdlemk19u1  41554  cdleml1N  41561  cdleml2N  41562  cdleml3N  41563  dia2dimlem6  41654  cdlemn2  41780  cdlemn2a  41781  cdlemn5pre  41785  cdlemn10  41791  cdlemn11c  41794  cdlemn11pre  41795  dihjustlem  41801  dihjust  41802  lclkrlem2y  42116  aks6d1c1  42694  relexpmulnn  44246  ormkglobd  47412  natglobalincr  47414  lincreslvec3  49065  iscnrm3llem1  49531  iscnrm3l  49533  swapffunc  49864  fucofunc  49941  amgmwlem  50384