Theorem simp21 1204

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  simp121  1303  simp221  1312  simp321  1321  omeulem1  8219  cofsmo  9730  axdc4lem  9916  0catg  17017  funcoppc  17205  funcres  17226  catcisolem  17433  1stfcl  17514  2ndfcl  17515  prfcl  17520  evlfcl  17539  curf1cl  17545  curfcl  17549  hofcl  17576  mulgdirlem  18326  mdetunilem4  21316  mdetuni0  21322  mdetmul  21324  prdsxmetlem  23071  isosctrlem3  25506  isosctr  25507  amgmlem  25675  f1otrg  26765  colinearalg  26804  ax5seglem6  26828  ax5seg  26832  axpasch  26835  axeuclidlem  26856  axeuclid  26857  uhgr2edg  27098  numclwlk1lem2  28255  ogrpsub  30869  ogrpaddlt  30870  ogrpsublt  30874  rhmdvd  31047  bnj1128  32491  mclspps  33063  nosupbnd2lem1  33484  cgrtr  33844  cgrtr3  33846  ofscom  33859  segconeq  33862  ifscgr  33896  btwnxfr  33908  colinearxfr  33927  lineext  33928  brofs2  33929  brifs2  33930  fscgr  33932  linecgr  33933  btwnconn1lem1  33939  btwnconn1lem2  33940  btwnconn1lem3  33941  btwnconn1lem4  33942  btwnconn1lem5  33943  btwnconn1lem6  33944  btwnconn1lem7  33945  seglecgr12im  33962  seglecgr12  33963  segletr  33966  broutsideof3  33978  outsideofeq  33982  lineunray  33999  lineelsb2  34000  linecom  34002  lshpkrlem5  36691  omlmod1i2N  36837  cvrnbtwn3  36853  cvrcmp  36860  cvrcmp2  36861  cvlexch2  36906  cvlexchb2  36908  cvlatexchb2  36912  cvlatexch2  36914  cvlatexch3  36915  cvlsupr7  36925  atnlej1  36956  atnlej2  36957  2llnneN  36986  cvratlem  36998  atcvrneN  37007  atcvrj1  37008  atlelt  37015  2atjm  37022  3noncolr2  37026  3noncolr1N  37027  3dimlem2  37036  3dim1  37044  3dim2  37045  1cvrat  37053  ps-1  37054  ps-2  37055  2atjlej  37056  hlatexch3N  37057  ps-2b  37059  3atlem1  37060  3atlem2  37061  3atlem5  37064  3atlem6  37065  llnle  37095  2atm  37104  ps-2c  37105  lplni2  37114  lplnle  37117  lplnnle2at  37118  lplnri3N  37132  llncvrlpln2  37134  2atmat  37138  2llnm2N  37145  2llnm4  37147  2llnmeqat  37148  lvolnle3at  37159  4atlem0ae  37171  4atlem0be  37172  4atlem3b  37175  4atlem9  37180  4atlem10a  37181  4atlem10  37183  4atlem11a  37184  4atlem12a  37187  4at2  37191  2lplnm2N  37198  lneq2at  37355  2llnma1b  37363  2llnma1  37364  2llnma3r  37365  2llnma2  37366  2llnma2rN  37367  cdlema1N  37368  paddasslem2  37398  paddasslem15  37411  paddasslem16  37412  pmodlem1  37423  pmodlem2  37424  pmod2iN  37426  hlmod1i  37433  atmod1i1m  37435  atmod2i1  37438  atmod2i2  37439  atmod3i1  37441  atmod3i2  37442  atmod4i1  37443  atmod4i2  37444  llnexchb2lem  37445  llnexch2N  37447  dalawlem3  37450  dalawlem4  37451  dalawlem5  37452  dalawlem6  37453  dalawlem7  37454  dalawlem8  37455  dalawlem9  37456  dalawlem11  37458  dalawlem12  37459  dalawlem13  37460  dalawlem15  37462  osumcllem9N  37541  pl42lem1N  37556  4atexlems  37629  4atex2  37654  4atex2-0bOLDN  37656  trlval4  37765  cdlemc5  37772  cdlemc6  37773  cdlemd2  37776  cdlemd4  37778  cdlemd6  37780  cdleme00a  37786  cdleme0e  37794  cdleme3g  37811  cdleme3h  37812  cdleme3  37814  cdleme4  37815  cdleme4a  37816  cdleme5  37817  cdleme9  37830  cdleme16aN  37836  cdleme11c  37838  cdleme11e  37840  cdleme11g  37842  cdleme11h  37843  cdleme11j  37844  cdleme11k  37845  cdleme11l  37846  cdleme11  37847  cdleme12  37848  cdleme14  37850  cdleme15c  37853  cdleme16b  37856  cdleme16c  37857  cdleme16d  37858  cdleme16e  37859  cdleme16f  37860  cdleme0nex  37867  cdleme18a  37868  cdleme18c  37870  cdleme18d  37872  cdlemednpq  37876  cdlemednuN  37877  cdleme20zN  37878  cdleme20y  37879  cdleme19a  37880  cdleme19b  37881  cdleme19d  37883  cdleme19e  37884  cdleme20aN  37886  cdleme20bN  37887  cdleme20c  37888  cdleme20d  37889  cdleme20f  37891  cdleme20g  37892  cdleme20i  37894  cdleme20j  37895  cdleme20l1  37897  cdleme20l2  37898  cdleme20l  37899  cdleme20m  37900  cdleme21b  37903  cdleme21c  37904  cdleme21e  37908  cdleme21f  37909  cdleme22a  37917  cdleme22b  37918  cdleme22e  37921  cdleme22eALTN  37922  cdleme22f  37923  cdleme26eALTN  37938  cdleme26fALTN  37939  cdleme26f  37940  cdleme26f2ALTN  37941  cdleme26f2  37942  cdleme27N  37946  cdleme28a  37947  cdleme28b  37948  cdleme30a  37955  cdleme43fsv1snlem  37997  cdlemefs31fv1  38001  cdlemefs45eN  38008  cdleme32b  38019  cdleme32c  38020  cdleme32d  38021  cdleme35h  38033  cdleme36a  38037  cdleme36m  38038  cdleme37m  38039  cdleme40m  38044  cdleme40n  38045  cdleme41sn3aw  38051  cdleme41sn4aw  38052  cdleme41fva11  38054  cdleme42k  38061  cdleme43cN  38068  cdleme43dN  38069  cdleme46f2g1  38071  cdlemeg47rv2  38087  cdlemeg46sfg  38097  cdlemeg46fjgN  38098  cdlemeg46rjgN  38099  cdlemeg46fjv  38100  cdlemeg46frv  38102  cdlemeg46vrg  38104  cdlemeg46rgv  38105  cdlemeg46req  38106  cdlemeg46gfv  38107  cdlemg4a  38185  cdlemg4d  38190  cdlemg4e  38191  cdlemg4f  38192  cdlemg4g  38193  cdlemg4  38194  cdlemg6d  38198  cdlemg6e  38199  cdlemg8b  38205  cdlemg8c  38206  cdlemg9a  38209  cdlemg9b  38210  cdlemg10a  38217  cdlemg10  38218  cdlemg12a  38220  cdlemg12b  38221  cdlemg12f  38225  cdlemg12g  38226  cdlemg12  38227  cdlemg17dN  38240  cdlemg17dALTN  38241  cdlemg17e  38242  cdlemg17f  38243  cdlemg17g  38244  cdlemg17h  38245  cdlemg17i  38246  cdlemg17pq  38249  cdlemg17iqN  38251  cdlemg17  38254  cdlemg18b  38256  cdlemg18c  38257  cdlemg19a  38260  cdlemg19  38261  cdlemg28a  38270  cdlemg27b  38273  cdlemg28b  38280  cdlemg28  38281  cdlemg33a  38283  cdlemg33b  38284  cdlemg33c  38285  cdlemg33d  38286  cdlemg33e  38287  cdlemg33  38288  cdlemg35  38290  cdlemg36  38291  cdlemg44a  38308  cdlemh  38394  cdlemi2  38396  cdlemj1  38398  tendocan  38401  cdlemk5a  38412  cdlemki  38418  cdlemkvcl  38419  cdlemk10  38420  cdlemksv2  38424  cdlemkole  38430  cdlemk14  38431  cdlemk15  38432  cdlemk16a  38433  cdlemk16  38434  cdlemk17  38435  cdlemk18  38445  cdlemk19  38446  cdlemkoatnle-2N  38452  cdlemk13-2N  38453  cdlemkole-2N  38454  cdlemk14-2N  38455  cdlemk15-2N  38456  cdlemk16-2N  38457  cdlemk17-2N  38458  cdlemk18-2N  38463  cdlemk19-2N  38464  cdlemk30  38471  cdlemk18-3N  38477  cdlemk23-3  38479  cdlemk25-3  38481  cdlemk27-3  38484  cdlemk37  38491  cdlemkfid1N  38498  cdlemkid1  38499  cdlemky  38503  cdlemk11ta  38506  cdlemk47  38526  cdlemk48  38527  cdlemk49  38528  cdlemk50  38529  cdlemk51  38530  cdlemk52  38531  cdlemk53a  38532  cdlemk54  38535  cdlemk39u1  38544  cdlemk19u1  38546  cdleml1N  38553  cdleml2N  38554  cdleml3N  38555  dia2dimlem6  38646  cdlemn2  38772  cdlemn2a  38773  cdlemn5pre  38777  cdlemn10  38783  cdlemn11c  38786  cdlemn11pre  38787  dihjustlem  38793  dihjust  38794  lclkrlem2y  39108  relexpmulnn  40784  lincreslvec3  45257  amgmwlem  45722