Theorem simp21 1223

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  simp121  1322  simp221  1331  simp321  1340  omeulem1  8563  cofsmo  10249  axdc4lem  10435  0catg  17740  funcoppc  17928  funcres  17949  catcisolem  18163  1stfcl  18249  2ndfcl  18250  prfcl  18255  evlfcl  18274  curf1cl  18280  curfcl  18284  hofcl  18311  mulgdirlem  19167  ogrpsub  20203  ogrpaddlt  20204  ogrpsublt  20208  mdetunilem4  22737  mdetuni0  22743  mdetmul  22745  prdsxmetlem  24490  isosctrlem3  26947  isosctr  26948  amgmlem  27116  nosupbnd2lem1  27841  addsass  28160  f1otrg  29157  colinearalg  29197  ax5seglem6  29221  ax5seg  29225  axpasch  29228  axeuclidlem  29249  axeuclid  29250  uhgr2edg  29495  numclwlk1lem2  30658  rhmdvd  33583  bnj1128  35319  mclspps  35971  cgrtr  36379  cgrtr3  36381  ofscom  36394  segconeq  36397  ifscgr  36431  btwnxfr  36443  colinearxfr  36462  lineext  36463  brofs2  36464  brifs2  36465  fscgr  36467  linecgr  36468  btwnconn1lem1  36474  btwnconn1lem2  36475  btwnconn1lem3  36476  btwnconn1lem4  36477  btwnconn1lem5  36478  btwnconn1lem6  36479  btwnconn1lem7  36480  seglecgr12im  36497  seglecgr12  36498  segletr  36501  broutsideof3  36513  outsideofeq  36517  lineunray  36534  lineelsb2  36535  linecom  36537  lshpkrlem5  39773  omlmod1i2N  39919  cvrnbtwn3  39935  cvrcmp  39942  cvrcmp2  39943  cvlexch2  39988  cvlexchb2  39990  cvlatexchb2  39994  cvlatexch2  39996  cvlatexch3  39997  cvlsupr7  40007  atnlej1  40038  atnlej2  40039  2llnneN  40068  cvratlem  40080  atcvrneN  40089  atcvrj1  40090  atlelt  40097  2atjm  40104  3noncolr2  40108  3noncolr1N  40109  3dimlem2  40118  3dim1  40126  3dim2  40127  1cvrat  40135  ps-1  40136  ps-2  40137  2atjlej  40138  hlatexch3N  40139  ps-2b  40141  3atlem1  40142  3atlem2  40143  3atlem5  40146  3atlem6  40147  llnle  40177  2atm  40186  ps-2c  40187  lplni2  40196  lplnle  40199  lplnnle2at  40200  lplnri3N  40214  llncvrlpln2  40216  2atmat  40220  2llnm2N  40227  2llnm4  40229  2llnmeqat  40230  lvolnle3at  40241  4atlem0ae  40253  4atlem0be  40254  4atlem3b  40257  4atlem9  40262  4atlem10a  40263  4atlem10  40265  4atlem11a  40266  4atlem12a  40269  4at2  40273  2lplnm2N  40280  lneq2at  40437  2llnma1b  40445  2llnma1  40446  2llnma3r  40447  2llnma2  40448  2llnma2rN  40449  cdlema1N  40450  paddasslem2  40480  paddasslem15  40493  paddasslem16  40494  pmodlem1  40505  pmodlem2  40506  pmod2iN  40508  hlmod1i  40515  atmod1i1m  40517  atmod2i1  40520  atmod2i2  40521  atmod3i1  40523  atmod3i2  40524  atmod4i1  40525  atmod4i2  40526  llnexchb2lem  40527  llnexch2N  40529  dalawlem3  40532  dalawlem4  40533  dalawlem5  40534  dalawlem6  40535  dalawlem7  40536  dalawlem8  40537  dalawlem9  40538  dalawlem11  40540  dalawlem12  40541  dalawlem13  40542  dalawlem15  40544  osumcllem9N  40623  pl42lem1N  40638  4atexlems  40711  4atex2  40736  4atex2-0bOLDN  40738  trlval4  40847  cdlemc5  40854  cdlemc6  40855  cdlemd2  40858  cdlemd4  40860  cdlemd6  40862  cdleme00a  40868  cdleme0e  40876  cdleme3g  40893  cdleme3h  40894  cdleme3  40896  cdleme4  40897  cdleme4a  40898  cdleme5  40899  cdleme9  40912  cdleme16aN  40918  cdleme11c  40920  cdleme11e  40922  cdleme11g  40924  cdleme11h  40925  cdleme11j  40926  cdleme11k  40927  cdleme11l  40928  cdleme11  40929  cdleme12  40930  cdleme14  40932  cdleme15c  40935  cdleme16b  40938  cdleme16c  40939  cdleme16d  40940  cdleme16e  40941  cdleme16f  40942  cdleme0nex  40949  cdleme18a  40950  cdleme18c  40952  cdleme18d  40954  cdlemednpq  40958  cdlemednuN  40959  cdleme20zN  40960  cdleme20y  40961  cdleme19a  40962  cdleme19b  40963  cdleme19d  40965  cdleme19e  40966  cdleme20aN  40968  cdleme20bN  40969  cdleme20c  40970  cdleme20d  40971  cdleme20f  40973  cdleme20g  40974  cdleme20i  40976  cdleme20j  40977  cdleme20l1  40979  cdleme20l2  40980  cdleme20l  40981  cdleme20m  40982  cdleme21b  40985  cdleme21c  40986  cdleme21e  40990  cdleme21f  40991  cdleme22a  40999  cdleme22b  41000  cdleme22e  41003  cdleme22eALTN  41004  cdleme22f  41005  cdleme26eALTN  41020  cdleme26fALTN  41021  cdleme26f  41022  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme27N  41028  cdleme28a  41029  cdleme28b  41030  cdleme30a  41037  cdleme43fsv1snlem  41079  cdlemefs31fv1  41083  cdlemefs45eN  41090  cdleme32b  41101  cdleme32c  41102  cdleme32d  41103  cdleme35h  41115  cdleme36a  41119  cdleme36m  41120  cdleme37m  41121  cdleme40m  41126  cdleme40n  41127  cdleme41sn3aw  41133  cdleme41sn4aw  41134  cdleme41fva11  41136  cdleme42k  41143  cdleme43cN  41150  cdleme43dN  41151  cdleme46f2g1  41153  cdlemeg47rv2  41169  cdlemeg46sfg  41179  cdlemeg46fjgN  41180  cdlemeg46rjgN  41181  cdlemeg46fjv  41182  cdlemeg46frv  41184  cdlemeg46vrg  41186  cdlemeg46rgv  41187  cdlemeg46req  41188  cdlemeg46gfv  41189  cdlemg4a  41267  cdlemg4d  41272  cdlemg4e  41273  cdlemg4f  41274  cdlemg4g  41275  cdlemg4  41276  cdlemg6d  41280  cdlemg6e  41281  cdlemg8b  41287  cdlemg8c  41288  cdlemg9a  41291  cdlemg9b  41292  cdlemg10a  41299  cdlemg10  41300  cdlemg12a  41302  cdlemg12b  41303  cdlemg12f  41307  cdlemg12g  41308  cdlemg12  41309  cdlemg17dN  41322  cdlemg17dALTN  41323  cdlemg17e  41324  cdlemg17f  41325  cdlemg17g  41326  cdlemg17h  41327  cdlemg17i  41328  cdlemg17pq  41331  cdlemg17iqN  41333  cdlemg17  41336  cdlemg18b  41338  cdlemg18c  41339  cdlemg19a  41342  cdlemg19  41343  cdlemg28a  41352  cdlemg27b  41355  cdlemg28b  41362  cdlemg28  41363  cdlemg33a  41365  cdlemg33b  41366  cdlemg33c  41367  cdlemg33d  41368  cdlemg33e  41369  cdlemg33  41370  cdlemg35  41372  cdlemg36  41373  cdlemg44a  41390  cdlemh  41476  cdlemi2  41478  cdlemj1  41480  tendocan  41483  cdlemk5a  41494  cdlemki  41500  cdlemkvcl  41501  cdlemk10  41502  cdlemksv2  41506  cdlemkole  41512  cdlemk14  41513  cdlemk15  41514  cdlemk16a  41515  cdlemk16  41516  cdlemk17  41517  cdlemk18  41527  cdlemk19  41528  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk30  41553  cdlemk18-3N  41559  cdlemk23-3  41561  cdlemk25-3  41563  cdlemk27-3  41566  cdlemk37  41573  cdlemkfid1N  41580  cdlemkid1  41581  cdlemky  41585  cdlemk11ta  41588  cdlemk47  41608  cdlemk48  41609  cdlemk49  41610  cdlemk50  41611  cdlemk51  41612  cdlemk52  41613  cdlemk53a  41614  cdlemk54  41617  cdlemk39u1  41626  cdlemk19u1  41628  cdleml1N  41635  cdleml2N  41636  cdleml3N  41637  dia2dimlem6  41728  cdlemn2  41854  cdlemn2a  41855  cdlemn5pre  41859  cdlemn10  41865  cdlemn11c  41868  cdlemn11pre  41869  dihjustlem  41875  dihjust  41876  lclkrlem2y  42190  aks6d1c1  42768  relexpmulnn  44320  ormkglobd  47476  natglobalincr  47478  lincreslvec3  49140  iscnrm3llem1  49605  iscnrm3l  49607  swapffunc  49938  fucofunc  50015  amgmwlem  50458