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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp121  1303  simp221  1312  simp321  1321  omeulem1  8389  cofsmo  10009  axdc4lem  10195  0catg  17378  funcoppc  17571  funcres  17592  catcisolem  17806  1stfcl  17895  2ndfcl  17896  prfcl  17901  evlfcl  17921  curf1cl  17927  curfcl  17931  hofcl  17958  mulgdirlem  18715  mdetunilem4  21745  mdetuni0  21751  mdetmul  21753  prdsxmetlem  23502  isosctrlem3  25951  isosctr  25952  amgmlem  26120  f1otrg  27213  colinearalg  27259  ax5seglem6  27283  ax5seg  27287  axpasch  27290  axeuclidlem  27311  axeuclid  27312  uhgr2edg  27556  numclwlk1lem2  28713  ogrpsub  31321  ogrpaddlt  31322  ogrpsublt  31326  rhmdvd  31499  bnj1128  32949  mclspps  33525  nosupbnd2lem1  33897  cgrtr  34273  cgrtr3  34275  ofscom  34288  segconeq  34291  ifscgr  34325  btwnxfr  34337  colinearxfr  34356  lineext  34357  brofs2  34358  brifs2  34359  fscgr  34361  linecgr  34362  btwnconn1lem1  34368  btwnconn1lem2  34369  btwnconn1lem3  34370  btwnconn1lem4  34371  btwnconn1lem5  34372  btwnconn1lem6  34373  btwnconn1lem7  34374  seglecgr12im  34391  seglecgr12  34392  segletr  34395  broutsideof3  34407  outsideofeq  34411  lineunray  34428  lineelsb2  34429  linecom  34431  lshpkrlem5  37107  omlmod1i2N  37253  cvrnbtwn3  37269  cvrcmp  37276  cvrcmp2  37277  cvlexch2  37322  cvlexchb2  37324  cvlatexchb2  37328  cvlatexch2  37330  cvlatexch3  37331  cvlsupr7  37341  atnlej1  37372  atnlej2  37373  2llnneN  37402  cvratlem  37414  atcvrneN  37423  atcvrj1  37424  atlelt  37431  2atjm  37438  3noncolr2  37442  3noncolr1N  37443  3dimlem2  37452  3dim1  37460  3dim2  37461  1cvrat  37469  ps-1  37470  ps-2  37471  2atjlej  37472  hlatexch3N  37473  ps-2b  37475  3atlem1  37476  3atlem2  37477  3atlem5  37480  3atlem6  37481  llnle  37511  2atm  37520  ps-2c  37521  lplni2  37530  lplnle  37533  lplnnle2at  37534  lplnri3N  37548  llncvrlpln2  37550  2atmat  37554  2llnm2N  37561  2llnm4  37563  2llnmeqat  37564  lvolnle3at  37575  4atlem0ae  37587  4atlem0be  37588  4atlem3b  37591  4atlem9  37596  4atlem10a  37597  4atlem10  37599  4atlem11a  37600  4atlem12a  37603  4at2  37607  2lplnm2N  37614  lneq2at  37771  2llnma1b  37779  2llnma1  37780  2llnma3r  37781  2llnma2  37782  2llnma2rN  37783  cdlema1N  37784  paddasslem2  37814  paddasslem15  37827  paddasslem16  37828  pmodlem1  37839  pmodlem2  37840  pmod2iN  37842  hlmod1i  37849  atmod1i1m  37851  atmod2i1  37854  atmod2i2  37855  atmod3i1  37857  atmod3i2  37858  atmod4i1  37859  atmod4i2  37860  llnexchb2lem  37861  llnexch2N  37863  dalawlem3  37866  dalawlem4  37867  dalawlem5  37868  dalawlem6  37869  dalawlem7  37870  dalawlem8  37871  dalawlem9  37872  dalawlem11  37874  dalawlem12  37875  dalawlem13  37876  dalawlem15  37878  osumcllem9N  37957  pl42lem1N  37972  4atexlems  38045  4atex2  38070  4atex2-0bOLDN  38072  trlval4  38181  cdlemc5  38188  cdlemc6  38189  cdlemd2  38192  cdlemd4  38194  cdlemd6  38196  cdleme00a  38202  cdleme0e  38210  cdleme3g  38227  cdleme3h  38228  cdleme3  38230  cdleme4  38231  cdleme4a  38232  cdleme5  38233  cdleme9  38246  cdleme16aN  38252  cdleme11c  38254  cdleme11e  38256  cdleme11g  38258  cdleme11h  38259  cdleme11j  38260  cdleme11k  38261  cdleme11l  38262  cdleme11  38263  cdleme12  38264  cdleme14  38266  cdleme15c  38269  cdleme16b  38272  cdleme16c  38273  cdleme16d  38274  cdleme16e  38275  cdleme16f  38276  cdleme0nex  38283  cdleme18a  38284  cdleme18c  38286  cdleme18d  38288  cdlemednpq  38292  cdlemednuN  38293  cdleme20zN  38294  cdleme20y  38295  cdleme19a  38296  cdleme19b  38297  cdleme19d  38299  cdleme19e  38300  cdleme20aN  38302  cdleme20bN  38303  cdleme20c  38304  cdleme20d  38305  cdleme20f  38307  cdleme20g  38308  cdleme20i  38310  cdleme20j  38311  cdleme20l1  38313  cdleme20l2  38314  cdleme20l  38315  cdleme20m  38316  cdleme21b  38319  cdleme21c  38320  cdleme21e  38324  cdleme21f  38325  cdleme22a  38333  cdleme22b  38334  cdleme22e  38337  cdleme22eALTN  38338  cdleme22f  38339  cdleme26eALTN  38354  cdleme26fALTN  38355  cdleme26f  38356  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme27N  38362  cdleme28a  38363  cdleme28b  38364  cdleme30a  38371  cdleme43fsv1snlem  38413  cdlemefs31fv1  38417  cdlemefs45eN  38424  cdleme32b  38435  cdleme32c  38436  cdleme32d  38437  cdleme35h  38449  cdleme36a  38453  cdleme36m  38454  cdleme37m  38455  cdleme40m  38460  cdleme40n  38461  cdleme41sn3aw  38467  cdleme41sn4aw  38468  cdleme41fva11  38470  cdleme42k  38477  cdleme43cN  38484  cdleme43dN  38485  cdleme46f2g1  38487  cdlemeg47rv2  38503  cdlemeg46sfg  38513  cdlemeg46fjgN  38514  cdlemeg46rjgN  38515  cdlemeg46fjv  38516  cdlemeg46frv  38518  cdlemeg46vrg  38520  cdlemeg46rgv  38521  cdlemeg46req  38522  cdlemeg46gfv  38523  cdlemg4a  38601  cdlemg4d  38606  cdlemg4e  38607  cdlemg4f  38608  cdlemg4g  38609  cdlemg4  38610  cdlemg6d  38614  cdlemg6e  38615  cdlemg8b  38621  cdlemg8c  38622  cdlemg9a  38625  cdlemg9b  38626  cdlemg10a  38633  cdlemg10  38634  cdlemg12a  38636  cdlemg12b  38637  cdlemg12f  38641  cdlemg12g  38642  cdlemg12  38643  cdlemg17dN  38656  cdlemg17dALTN  38657  cdlemg17e  38658  cdlemg17f  38659  cdlemg17g  38660  cdlemg17h  38661  cdlemg17i  38662  cdlemg17pq  38665  cdlemg17iqN  38667  cdlemg17  38670  cdlemg18b  38672  cdlemg18c  38673  cdlemg19a  38676  cdlemg19  38677  cdlemg28a  38686  cdlemg27b  38689  cdlemg28b  38696  cdlemg28  38697  cdlemg33a  38699  cdlemg33b  38700  cdlemg33c  38701  cdlemg33d  38702  cdlemg33e  38703  cdlemg33  38704  cdlemg35  38706  cdlemg36  38707  cdlemg44a  38724  cdlemh  38810  cdlemi2  38812  cdlemj1  38814  tendocan  38817  cdlemk5a  38828  cdlemki  38834  cdlemkvcl  38835  cdlemk10  38836  cdlemksv2  38840  cdlemkole  38846  cdlemk14  38847  cdlemk15  38848  cdlemk16a  38849  cdlemk16  38850  cdlemk17  38851  cdlemk18  38861  cdlemk19  38862  cdlemkoatnle-2N  38868  cdlemk13-2N  38869  cdlemkole-2N  38870  cdlemk14-2N  38871  cdlemk15-2N  38872  cdlemk16-2N  38873  cdlemk17-2N  38874  cdlemk18-2N  38879  cdlemk19-2N  38880  cdlemk30  38887  cdlemk18-3N  38893  cdlemk23-3  38895  cdlemk25-3  38897  cdlemk27-3  38900  cdlemk37  38907  cdlemkfid1N  38914  cdlemkid1  38915  cdlemky  38919  cdlemk11ta  38922  cdlemk47  38942  cdlemk48  38943  cdlemk49  38944  cdlemk50  38945  cdlemk51  38946  cdlemk52  38947  cdlemk53a  38948  cdlemk54  38951  cdlemk39u1  38960  cdlemk19u1  38962  cdleml1N  38969  cdleml2N  38970  cdleml3N  38971  dia2dimlem6  39062  cdlemn2  39188  cdlemn2a  39189  cdlemn5pre  39193  cdlemn10  39199  cdlemn11c  39202  cdlemn11pre  39203  dihjustlem  39209  dihjust  39210  lclkrlem2y  39524  relexpmulnn  41270  lincreslvec3  45775  iscnrm3llem1  46195  iscnrm3l  46197  amgmwlem  46458