Theorem simp21 1202

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  simp121  1301  simp221  1310  simp321  1319  omeulem1  8208  cofsmo  9691  axdc4lem  9877  0catg  16958  funcoppc  17145  funcres  17166  catcisolem  17366  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  mulgdirlem  18258  mdetunilem4  21224  mdetuni0  21230  mdetmul  21232  prdsxmetlem  22978  isosctrlem3  25398  isosctr  25399  amgmlem  25567  f1otrg  26657  colinearalg  26696  ax5seglem6  26720  ax5seg  26724  axpasch  26727  axeuclidlem  26748  axeuclid  26749  uhgr2edg  26990  numclwlk1lem2  28149  ogrpsub  30717  ogrpaddlt  30718  ogrpsublt  30722  rhmdvd  30894  bnj1128  32262  mclspps  32831  nosupbnd2lem1  33215  cgrtr  33453  cgrtr3  33455  ofscom  33468  segconeq  33471  ifscgr  33505  btwnxfr  33517  colinearxfr  33536  lineext  33537  brofs2  33538  brifs2  33539  fscgr  33541  linecgr  33542  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem7  33554  seglecgr12im  33571  seglecgr12  33572  segletr  33575  broutsideof3  33587  outsideofeq  33591  lineunray  33608  lineelsb2  33609  linecom  33611  lshpkrlem5  36265  omlmod1i2N  36411  cvrnbtwn3  36427  cvrcmp  36434  cvrcmp2  36435  cvlexch2  36480  cvlexchb2  36482  cvlatexchb2  36486  cvlatexch2  36488  cvlatexch3  36489  cvlsupr7  36499  atnlej1  36530  atnlej2  36531  2llnneN  36560  cvratlem  36572  atcvrneN  36581  atcvrj1  36582  atlelt  36589  2atjm  36596  3noncolr2  36600  3noncolr1N  36601  3dimlem2  36610  3dim1  36618  3dim2  36619  1cvrat  36627  ps-1  36628  ps-2  36629  2atjlej  36630  hlatexch3N  36631  ps-2b  36633  3atlem1  36634  3atlem2  36635  3atlem5  36638  3atlem6  36639  llnle  36669  2atm  36678  ps-2c  36679  lplni2  36688  lplnle  36691  lplnnle2at  36692  lplnri3N  36706  llncvrlpln2  36708  2atmat  36712  2llnm2N  36719  2llnm4  36721  2llnmeqat  36722  lvolnle3at  36733  4atlem0ae  36745  4atlem0be  36746  4atlem3b  36749  4atlem9  36754  4atlem10a  36755  4atlem10  36757  4atlem11a  36758  4atlem12a  36761  4at2  36765  2lplnm2N  36772  lneq2at  36929  2llnma1b  36937  2llnma1  36938  2llnma3r  36939  2llnma2  36940  2llnma2rN  36941  cdlema1N  36942  paddasslem2  36972  paddasslem15  36985  paddasslem16  36986  pmodlem1  36997  pmodlem2  36998  pmod2iN  37000  hlmod1i  37007  atmod1i1m  37009  atmod2i1  37012  atmod2i2  37013  atmod3i1  37015  atmod3i2  37016  atmod4i1  37017  atmod4i2  37018  llnexchb2lem  37019  llnexch2N  37021  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem13  37034  dalawlem15  37036  osumcllem9N  37115  pl42lem1N  37130  4atexlems  37203  4atex2  37228  4atex2-0bOLDN  37230  trlval4  37339  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdlemd4  37352  cdlemd6  37354  cdleme00a  37360  cdleme0e  37368  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme9  37404  cdleme16aN  37410  cdleme11c  37412  cdleme11e  37414  cdleme11g  37416  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme11l  37420  cdleme11  37421  cdleme12  37422  cdleme14  37424  cdleme15c  37427  cdleme16b  37430  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme0nex  37441  cdleme18a  37442  cdleme18c  37444  cdleme18d  37446  cdlemednpq  37450  cdlemednuN  37451  cdleme20zN  37452  cdleme20y  37453  cdleme19a  37454  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20aN  37460  cdleme20bN  37461  cdleme20c  37462  cdleme20d  37463  cdleme20f  37465  cdleme20g  37466  cdleme20i  37468  cdleme20j  37469  cdleme20l1  37471  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21b  37477  cdleme21c  37478  cdleme21e  37482  cdleme21f  37483  cdleme22a  37491  cdleme22b  37492  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme26eALTN  37512  cdleme26fALTN  37513  cdleme26f  37514  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme27N  37520  cdleme28a  37521  cdleme28b  37522  cdleme30a  37529  cdleme43fsv1snlem  37571  cdlemefs31fv1  37575  cdlemefs45eN  37582  cdleme32b  37593  cdleme32c  37594  cdleme32d  37595  cdleme35h  37607  cdleme36a  37611  cdleme36m  37612  cdleme37m  37613  cdleme40m  37618  cdleme40n  37619  cdleme41sn3aw  37625  cdleme41sn4aw  37626  cdleme41fva11  37628  cdleme42k  37635  cdleme43cN  37642  cdleme43dN  37643  cdleme46f2g1  37645  cdlemeg47rv2  37661  cdlemeg46sfg  37671  cdlemeg46fjgN  37672  cdlemeg46rjgN  37673  cdlemeg46fjv  37674  cdlemeg46frv  37676  cdlemeg46vrg  37678  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemeg46gfv  37681  cdlemg4a  37759  cdlemg4d  37764  cdlemg4e  37765  cdlemg4f  37766  cdlemg4g  37767  cdlemg4  37768  cdlemg6d  37772  cdlemg6e  37773  cdlemg8b  37779  cdlemg8c  37780  cdlemg9a  37783  cdlemg9b  37784  cdlemg10a  37791  cdlemg10  37792  cdlemg12a  37794  cdlemg12b  37795  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg17dN  37814  cdlemg17dALTN  37815  cdlemg17e  37816  cdlemg17f  37817  cdlemg17g  37818  cdlemg17h  37819  cdlemg17i  37820  cdlemg17pq  37823  cdlemg17iqN  37825  cdlemg17  37828  cdlemg18b  37830  cdlemg18c  37831  cdlemg19a  37834  cdlemg19  37835  cdlemg28a  37844  cdlemg27b  37847  cdlemg28b  37854  cdlemg28  37855  cdlemg33a  37857  cdlemg33b  37858  cdlemg33c  37859  cdlemg33d  37860  cdlemg33e  37861  cdlemg33  37862  cdlemg35  37864  cdlemg36  37865  cdlemg44a  37882  cdlemh  37968  cdlemi2  37970  cdlemj1  37972  tendocan  37975  cdlemk5a  37986  cdlemki  37992  cdlemkvcl  37993  cdlemk10  37994  cdlemksv2  37998  cdlemkole  38004  cdlemk14  38005  cdlemk15  38006  cdlemk16a  38007  cdlemk16  38008  cdlemk17  38009  cdlemk18  38019  cdlemk19  38020  cdlemkoatnle-2N  38026  cdlemk13-2N  38027  cdlemkole-2N  38028  cdlemk14-2N  38029  cdlemk15-2N  38030  cdlemk16-2N  38031  cdlemk17-2N  38032  cdlemk18-2N  38037  cdlemk19-2N  38038  cdlemk30  38045  cdlemk18-3N  38051  cdlemk23-3  38053  cdlemk25-3  38055  cdlemk27-3  38058  cdlemk37  38065  cdlemkfid1N  38072  cdlemkid1  38073  cdlemky  38077  cdlemk11ta  38080  cdlemk47  38100  cdlemk48  38101  cdlemk49  38102  cdlemk50  38103  cdlemk51  38104  cdlemk52  38105  cdlemk53a  38106  cdlemk54  38109  cdlemk39u1  38118  cdlemk19u1  38120  cdleml1N  38127  cdleml2N  38128  cdleml3N  38129  dia2dimlem6  38220  cdlemn2  38346  cdlemn2a  38347  cdlemn5pre  38351  cdlemn10  38357  cdlemn11c  38360  cdlemn11pre  38361  dihjustlem  38367  dihjust  38368  lclkrlem2y  38682  relexpmulnn  40074  lincreslvec3  44557  amgmwlem  44923