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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp121  1324  simp221  1333  simp321  1342  omeulem1  8583  cofsmo  10340  axdc4lem  10526  0catg  17855  funcoppc  18043  funcres  18064  catcisolem  18278  1stfcl  18364  2ndfcl  18365  prfcl  18370  evlfcl  18389  curf1cl  18395  curfcl  18399  hofcl  18426  mulgdirlem  19308  ogrpsub  20344  ogrpaddlt  20345  ogrpsublt  20349  mdetunilem4  22923  mdetuni0  22929  mdetmul  22931  prdsxmetlem  24680  isosctrlem3  27141  isosctr  27142  amgmlem  27310  nosupbnd2lem1  28065  addsass  28384  f1otrg  29441  colinearalg  29481  ax5seglem6  29505  ax5seg  29509  axpasch  29512  axeuclidlem  29533  axeuclid  29534  uhgr2edg  29782  numclwlk1lem2  30964  rhmdvd  33878  bnj1128  35613  mclspps  36328  cgrtr  36737  cgrtr3  36739  ofscom  36752  segconeq  36755  ifscgr  36789  btwnxfr  36801  colinearxfr  36820  lineext  36821  brofs2  36822  brifs2  36823  fscgr  36825  linecgr  36826  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem3  36834  btwnconn1lem4  36835  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem7  36838  seglecgr12im  36855  seglecgr12  36856  segletr  36859  broutsideof3  36871  outsideofeq  36875  lineunray  36892  lineelsb2  36893  linecom  36895  lshpkrlem5  40151  omlmod1i2N  40297  cvrnbtwn3  40313  cvrcmp  40320  cvrcmp2  40321  cvlexch2  40366  cvlexchb2  40368  cvlatexchb2  40372  cvlatexch2  40374  cvlatexch3  40375  cvlsupr7  40385  atnlej1  40416  atnlej2  40417  2llnneN  40446  cvratlem  40458  atcvrneN  40467  atcvrj1  40468  atlelt  40475  2atjm  40482  3noncolr2  40486  3noncolr1N  40487  3dimlem2  40496  3dim1  40504  3dim2  40505  1cvrat  40513  ps-1  40514  ps-2  40515  2atjlej  40516  hlatexch3N  40517  ps-2b  40519  3atlem1  40520  3atlem2  40521  3atlem5  40524  3atlem6  40525  llnle  40555  2atm  40564  ps-2c  40565  lplni2  40574  lplnle  40577  lplnnle2at  40578  lplnri3N  40592  llncvrlpln2  40594  2atmat  40598  2llnm2N  40605  2llnm4  40607  2llnmeqat  40608  lvolnle3at  40619  4atlem0ae  40631  4atlem0be  40632  4atlem3b  40635  4atlem9  40640  4atlem10a  40641  4atlem10  40643  4atlem11a  40644  4atlem12a  40647  4at2  40651  2lplnm2N  40658  lneq2at  40815  2llnma1b  40823  2llnma1  40824  2llnma3r  40825  2llnma2  40826  2llnma2rN  40827  cdlema1N  40828  paddasslem2  40858  paddasslem15  40871  paddasslem16  40872  pmodlem1  40883  pmodlem2  40884  pmod2iN  40886  hlmod1i  40893  atmod1i1m  40895  atmod2i1  40898  atmod2i2  40899  atmod3i1  40901  atmod3i2  40902  atmod4i1  40903  atmod4i2  40904  llnexchb2lem  40905  llnexch2N  40907  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem13  40920  dalawlem15  40922  osumcllem9N  41001  pl42lem1N  41016  4atexlems  41089  4atex2  41114  4atex2-0bOLDN  41116  trlval4  41225  cdlemc5  41232  cdlemc6  41233  cdlemd2  41236  cdlemd4  41238  cdlemd6  41240  cdleme00a  41246  cdleme0e  41254  cdleme3g  41271  cdleme3h  41272  cdleme3  41274  cdleme4  41275  cdleme4a  41276  cdleme5  41277  cdleme9  41290  cdleme16aN  41296  cdleme11c  41298  cdleme11e  41300  cdleme11g  41302  cdleme11h  41303  cdleme11j  41304  cdleme11k  41305  cdleme11l  41306  cdleme11  41307  cdleme12  41308  cdleme14  41310  cdleme15c  41313  cdleme16b  41316  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme0nex  41327  cdleme18a  41328  cdleme18c  41330  cdleme18d  41332  cdlemednpq  41336  cdlemednuN  41337  cdleme20zN  41338  cdleme20y  41339  cdleme19a  41340  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20aN  41346  cdleme20bN  41347  cdleme20c  41348  cdleme20d  41349  cdleme20f  41351  cdleme20g  41352  cdleme20i  41354  cdleme20j  41355  cdleme20l1  41357  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme21b  41363  cdleme21c  41364  cdleme21e  41368  cdleme21f  41369  cdleme22a  41377  cdleme22b  41378  cdleme22e  41381  cdleme22eALTN  41382  cdleme22f  41383  cdleme26eALTN  41398  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme27N  41406  cdleme28a  41407  cdleme28b  41408  cdleme30a  41415  cdleme43fsv1snlem  41457  cdlemefs31fv1  41461  cdlemefs45eN  41468  cdleme32b  41479  cdleme32c  41480  cdleme32d  41481  cdleme35h  41493  cdleme36a  41497  cdleme36m  41498  cdleme37m  41499  cdleme40m  41504  cdleme40n  41505  cdleme41sn3aw  41511  cdleme41sn4aw  41512  cdleme41fva11  41514  cdleme42k  41521  cdleme43cN  41528  cdleme43dN  41529  cdleme46f2g1  41531  cdlemeg47rv2  41547  cdlemeg46sfg  41557  cdlemeg46fjgN  41558  cdlemeg46rjgN  41559  cdlemeg46fjv  41560  cdlemeg46frv  41562  cdlemeg46vrg  41564  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemeg46gfv  41567  cdlemg4a  41645  cdlemg4d  41650  cdlemg4e  41651  cdlemg4f  41652  cdlemg4g  41653  cdlemg4  41654  cdlemg6d  41658  cdlemg6e  41659  cdlemg8b  41665  cdlemg8c  41666  cdlemg9a  41669  cdlemg9b  41670  cdlemg10a  41677  cdlemg10  41678  cdlemg12a  41680  cdlemg12b  41681  cdlemg12f  41685  cdlemg12g  41686  cdlemg12  41687  cdlemg17dN  41700  cdlemg17dALTN  41701  cdlemg17e  41702  cdlemg17f  41703  cdlemg17g  41704  cdlemg17h  41705  cdlemg17i  41706  cdlemg17pq  41709  cdlemg17iqN  41711  cdlemg17  41714  cdlemg18b  41716  cdlemg18c  41717  cdlemg19a  41720  cdlemg19  41721  cdlemg28a  41730  cdlemg27b  41733  cdlemg28b  41740  cdlemg28  41741  cdlemg33a  41743  cdlemg33b  41744  cdlemg33c  41745  cdlemg33d  41746  cdlemg33e  41747  cdlemg33  41748  cdlemg35  41750  cdlemg36  41751  cdlemg44a  41768  cdlemh  41854  cdlemi2  41856  cdlemj1  41858  tendocan  41861  cdlemk5a  41872  cdlemki  41878  cdlemkvcl  41879  cdlemk10  41880  cdlemksv2  41884  cdlemkole  41890  cdlemk14  41891  cdlemk15  41892  cdlemk16a  41893  cdlemk16  41894  cdlemk17  41895  cdlemk18  41905  cdlemk19  41906  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk30  41931  cdlemk18-3N  41937  cdlemk23-3  41939  cdlemk25-3  41941  cdlemk27-3  41944  cdlemk37  41951  cdlemkfid1N  41958  cdlemkid1  41959  cdlemky  41963  cdlemk11ta  41966  cdlemk47  41986  cdlemk48  41987  cdlemk49  41988  cdlemk50  41989  cdlemk51  41990  cdlemk52  41991  cdlemk53a  41992  cdlemk54  41995  cdlemk39u1  42004  cdlemk19u1  42006  cdleml1N  42013  cdleml2N  42014  cdleml3N  42015  dia2dimlem6  42106  cdlemn2  42232  cdlemn2a  42233  cdlemn5pre  42237  cdlemn10  42243  cdlemn11c  42246  cdlemn11pre  42247  dihjustlem  42253  dihjust  42254  lclkrlem2y  42568  aks6d1c1  43146  relexpmulnn  44694  ormkglobd  47856  lincreslvec3  49563  iscnrm3llem1  50026  iscnrm3l  50028  swapffunc  50359  fucofunc  50436  amgmwlem  50956