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  8594  cofsmo  10351  axdc4lem  10537  0catg  17868  funcoppc  18056  funcres  18077  catcisolem  18291  1stfcl  18377  2ndfcl  18378  prfcl  18383  evlfcl  18402  curf1cl  18408  curfcl  18412  hofcl  18439  mulgdirlem  19321  ogrpsub  20357  ogrpaddlt  20358  ogrpsublt  20362  mdetunilem4  22936  mdetuni0  22942  mdetmul  22944  prdsxmetlem  24693  isosctrlem3  27154  isosctr  27155  amgmlem  27323  nosupbnd2lem1  28078  addsass  28397  f1otrg  29454  colinearalg  29494  ax5seglem6  29518  ax5seg  29522  axpasch  29525  axeuclidlem  29546  axeuclid  29547  uhgr2edg  29795  numclwlk1lem2  30977  rhmdvd  33932  bnj1128  35667  mclspps  36436  cgrtr  36850  cgrtr3  36852  ofscom  36865  segconeq  36868  ifscgr  36902  btwnxfr  36914  colinearxfr  36933  lineext  36934  brofs2  36935  brifs2  36936  fscgr  36938  linecgr  36939  btwnconn1lem1  36945  btwnconn1lem2  36946  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem5  36949  btwnconn1lem6  36950  btwnconn1lem7  36951  seglecgr12im  36968  seglecgr12  36969  segletr  36972  broutsideof3  36984  outsideofeq  36988  lineunray  37005  lineelsb2  37006  linecom  37008  lshpkrlem5  40265  omlmod1i2N  40411  cvrnbtwn3  40427  cvrcmp  40434  cvrcmp2  40435  cvlexch2  40480  cvlexchb2  40482  cvlatexchb2  40486  cvlatexch2  40488  cvlatexch3  40489  cvlsupr7  40499  atnlej1  40530  atnlej2  40531  2llnneN  40560  cvratlem  40572  atcvrneN  40581  atcvrj1  40582  atlelt  40589  2atjm  40596  3noncolr2  40600  3noncolr1N  40601  3dimlem2  40610  3dim1  40618  3dim2  40619  1cvrat  40627  ps-1  40628  ps-2  40629  2atjlej  40630  hlatexch3N  40631  ps-2b  40633  3atlem1  40634  3atlem2  40635  3atlem5  40638  3atlem6  40639  llnle  40669  2atm  40678  ps-2c  40679  lplni2  40688  lplnle  40691  lplnnle2at  40692  lplnri3N  40706  llncvrlpln2  40708  2atmat  40712  2llnm2N  40719  2llnm4  40721  2llnmeqat  40722  lvolnle3at  40733  4atlem0ae  40745  4atlem0be  40746  4atlem3b  40749  4atlem9  40754  4atlem10a  40755  4atlem10  40757  4atlem11a  40758  4atlem12a  40761  4at2  40765  2lplnm2N  40772  lneq2at  40929  2llnma1b  40937  2llnma1  40938  2llnma3r  40939  2llnma2  40940  2llnma2rN  40941  cdlema1N  40942  paddasslem2  40972  paddasslem15  40985  paddasslem16  40986  pmodlem1  40997  pmodlem2  40998  pmod2iN  41000  hlmod1i  41007  atmod1i1m  41009  atmod2i1  41012  atmod2i2  41013  atmod3i1  41015  atmod3i2  41016  atmod4i1  41017  atmod4i2  41018  llnexchb2lem  41019  llnexch2N  41021  dalawlem3  41024  dalawlem4  41025  dalawlem5  41026  dalawlem6  41027  dalawlem7  41028  dalawlem8  41029  dalawlem9  41030  dalawlem11  41032  dalawlem12  41033  dalawlem13  41034  dalawlem15  41036  osumcllem9N  41115  pl42lem1N  41130  4atexlems  41203  4atex2  41228  4atex2-0bOLDN  41230  trlval4  41339  cdlemc5  41346  cdlemc6  41347  cdlemd2  41350  cdlemd4  41352  cdlemd6  41354  cdleme00a  41360  cdleme0e  41368  cdleme3g  41385  cdleme3h  41386  cdleme3  41388  cdleme4  41389  cdleme4a  41390  cdleme5  41391  cdleme9  41404  cdleme16aN  41410  cdleme11c  41412  cdleme11e  41414  cdleme11g  41416  cdleme11h  41417  cdleme11j  41418  cdleme11k  41419  cdleme11l  41420  cdleme11  41421  cdleme12  41422  cdleme14  41424  cdleme15c  41427  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme0nex  41441  cdleme18a  41442  cdleme18c  41444  cdleme18d  41446  cdlemednpq  41450  cdlemednuN  41451  cdleme20zN  41452  cdleme20y  41453  cdleme19a  41454  cdleme19b  41455  cdleme19d  41457  cdleme19e  41458  cdleme20aN  41460  cdleme20bN  41461  cdleme20c  41462  cdleme20d  41463  cdleme20f  41465  cdleme20g  41466  cdleme20i  41468  cdleme20j  41469  cdleme20l1  41471  cdleme20l2  41472  cdleme20l  41473  cdleme20m  41474  cdleme21b  41477  cdleme21c  41478  cdleme21e  41482  cdleme21f  41483  cdleme22a  41491  cdleme22b  41492  cdleme22e  41495  cdleme22eALTN  41496  cdleme22f  41497  cdleme26eALTN  41512  cdleme26fALTN  41513  cdleme26f  41514  cdleme26f2ALTN  41515  cdleme26f2  41516  cdleme27N  41520  cdleme28a  41521  cdleme28b  41522  cdleme30a  41529  cdleme43fsv1snlem  41571  cdlemefs31fv1  41575  cdlemefs45eN  41582  cdleme32b  41593  cdleme32c  41594  cdleme32d  41595  cdleme35h  41607  cdleme36a  41611  cdleme36m  41612  cdleme37m  41613  cdleme40m  41618  cdleme40n  41619  cdleme41sn3aw  41625  cdleme41sn4aw  41626  cdleme41fva11  41628  cdleme42k  41635  cdleme43cN  41642  cdleme43dN  41643  cdleme46f2g1  41645  cdlemeg47rv2  41661  cdlemeg46sfg  41671  cdlemeg46fjgN  41672  cdlemeg46rjgN  41673  cdlemeg46fjv  41674  cdlemeg46frv  41676  cdlemeg46vrg  41678  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemeg46gfv  41681  cdlemg4a  41759  cdlemg4d  41764  cdlemg4e  41765  cdlemg4f  41766  cdlemg4g  41767  cdlemg4  41768  cdlemg6d  41772  cdlemg6e  41773  cdlemg8b  41779  cdlemg8c  41780  cdlemg9a  41783  cdlemg9b  41784  cdlemg10a  41791  cdlemg10  41792  cdlemg12a  41794  cdlemg12b  41795  cdlemg12f  41799  cdlemg12g  41800  cdlemg12  41801  cdlemg17dN  41814  cdlemg17dALTN  41815  cdlemg17e  41816  cdlemg17f  41817  cdlemg17g  41818  cdlemg17h  41819  cdlemg17i  41820  cdlemg17pq  41823  cdlemg17iqN  41825  cdlemg17  41828  cdlemg18b  41830  cdlemg18c  41831  cdlemg19a  41834  cdlemg19  41835  cdlemg28a  41844  cdlemg27b  41847  cdlemg28b  41854  cdlemg28  41855  cdlemg33a  41857  cdlemg33b  41858  cdlemg33c  41859  cdlemg33d  41860  cdlemg33e  41861  cdlemg33  41862  cdlemg35  41864  cdlemg36  41865  cdlemg44a  41882  cdlemh  41968  cdlemi2  41970  cdlemj1  41972  tendocan  41975  cdlemk5a  41986  cdlemki  41992  cdlemkvcl  41993  cdlemk10  41994  cdlemksv2  41998  cdlemkole  42004  cdlemk14  42005  cdlemk15  42006  cdlemk16a  42007  cdlemk16  42008  cdlemk17  42009  cdlemk18  42019  cdlemk19  42020  cdlemkoatnle-2N  42026  cdlemk13-2N  42027  cdlemkole-2N  42028  cdlemk14-2N  42029  cdlemk15-2N  42030  cdlemk16-2N  42031  cdlemk17-2N  42032  cdlemk18-2N  42037  cdlemk19-2N  42038  cdlemk30  42045  cdlemk18-3N  42051  cdlemk23-3  42053  cdlemk25-3  42055  cdlemk27-3  42058  cdlemk37  42065  cdlemkfid1N  42072  cdlemkid1  42073  cdlemky  42077  cdlemk11ta  42080  cdlemk47  42100  cdlemk48  42101  cdlemk49  42102  cdlemk50  42103  cdlemk51  42104  cdlemk52  42105  cdlemk53a  42106  cdlemk54  42109  cdlemk39u1  42118  cdlemk19u1  42120  cdleml1N  42127  cdleml2N  42128  cdleml3N  42129  dia2dimlem6  42220  cdlemn2  42346  cdlemn2a  42347  cdlemn5pre  42351  cdlemn10  42357  cdlemn11c  42360  cdlemn11pre  42361  dihjustlem  42367  dihjust  42368  lclkrlem2y  42682  aks6d1c1  43260  relexpmulnn  44803  ormkglobd  47981  lincreslvec3  49688  iscnrm3llem1  50157  iscnrm3l  50159  swapffunc  50498  fucofunc  50575  parmapfunc2  50868  parmapfunc  50869  amgmwlem  51156