Theorem simp21 1208

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp121  1307  simp221  1316  simp321  1325  omeulem1  8517  cofsmo  10191  axdc4lem  10377  0catg  17654  funcoppc  17842  funcres  17863  catcisolem  18077  1stfcl  18163  2ndfcl  18164  prfcl  18169  evlfcl  18188  curf1cl  18194  curfcl  18198  hofcl  18225  mulgdirlem  19081  ogrpsub  20112  ogrpaddlt  20113  ogrpsublt  20117  mdetunilem4  22580  mdetuni0  22586  mdetmul  22588  prdsxmetlem  24333  isosctrlem3  26784  isosctr  26785  amgmlem  26953  nosupbnd2lem1  27679  addsass  27997  f1otrg  28939  colinearalg  28979  ax5seglem6  29003  ax5seg  29007  axpasch  29010  axeuclidlem  29031  axeuclid  29032  uhgr2edg  29277  numclwlk1lem2  30440  rhmdvd  33384  bnj1128  35132  mclspps  35766  cgrtr  36174  cgrtr3  36176  ofscom  36189  segconeq  36192  ifscgr  36226  btwnxfr  36238  colinearxfr  36257  lineext  36258  brofs2  36259  brifs2  36260  fscgr  36262  linecgr  36263  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem7  36275  seglecgr12im  36292  seglecgr12  36293  segletr  36296  broutsideof3  36308  outsideofeq  36312  lineunray  36329  lineelsb2  36330  linecom  36332  lshpkrlem5  39560  omlmod1i2N  39706  cvrnbtwn3  39722  cvrcmp  39729  cvrcmp2  39730  cvlexch2  39775  cvlexchb2  39777  cvlatexchb2  39781  cvlatexch2  39783  cvlatexch3  39784  cvlsupr7  39794  atnlej1  39825  atnlej2  39826  2llnneN  39855  cvratlem  39867  atcvrneN  39876  atcvrj1  39877  atlelt  39884  2atjm  39891  3noncolr2  39895  3noncolr1N  39896  3dimlem2  39905  3dim1  39913  3dim2  39914  1cvrat  39922  ps-1  39923  ps-2  39924  2atjlej  39925  hlatexch3N  39926  ps-2b  39928  3atlem1  39929  3atlem2  39930  3atlem5  39933  3atlem6  39934  llnle  39964  2atm  39973  ps-2c  39974  lplni2  39983  lplnle  39986  lplnnle2at  39987  lplnri3N  40001  llncvrlpln2  40003  2atmat  40007  2llnm2N  40014  2llnm4  40016  2llnmeqat  40017  lvolnle3at  40028  4atlem0ae  40040  4atlem0be  40041  4atlem3b  40044  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem12a  40056  4at2  40060  2lplnm2N  40067  lneq2at  40224  2llnma1b  40232  2llnma1  40233  2llnma3r  40234  2llnma2  40235  2llnma2rN  40236  cdlema1N  40237  paddasslem2  40267  paddasslem15  40280  paddasslem16  40281  pmodlem1  40292  pmodlem2  40293  pmod2iN  40295  hlmod1i  40302  atmod1i1m  40304  atmod2i1  40307  atmod2i2  40308  atmod3i1  40310  atmod3i2  40311  atmod4i1  40312  atmod4i2  40313  llnexchb2lem  40314  llnexch2N  40316  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem13  40329  dalawlem15  40331  osumcllem9N  40410  pl42lem1N  40425  4atexlems  40498  4atex2  40523  4atex2-0bOLDN  40525  trlval4  40634  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdlemd4  40647  cdlemd6  40649  cdleme00a  40655  cdleme0e  40663  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme4a  40685  cdleme5  40686  cdleme9  40699  cdleme16aN  40705  cdleme11c  40707  cdleme11e  40709  cdleme11g  40711  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme11l  40715  cdleme11  40716  cdleme12  40717  cdleme14  40719  cdleme15c  40722  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme0nex  40736  cdleme18a  40737  cdleme18c  40739  cdleme18d  40741  cdlemednpq  40745  cdlemednuN  40746  cdleme20zN  40747  cdleme20y  40748  cdleme19a  40749  cdleme19b  40750  cdleme19d  40752  cdleme19e  40753  cdleme20aN  40755  cdleme20bN  40756  cdleme20c  40757  cdleme20d  40758  cdleme20f  40760  cdleme20g  40761  cdleme20i  40763  cdleme20j  40764  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21b  40772  cdleme21c  40773  cdleme21e  40777  cdleme21f  40778  cdleme22a  40786  cdleme22b  40787  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme26eALTN  40807  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme27N  40815  cdleme28a  40816  cdleme28b  40817  cdleme30a  40824  cdleme43fsv1snlem  40866  cdlemefs31fv1  40870  cdlemefs45eN  40877  cdleme32b  40888  cdleme32c  40889  cdleme32d  40890  cdleme35h  40902  cdleme36a  40906  cdleme36m  40907  cdleme37m  40908  cdleme40m  40913  cdleme40n  40914  cdleme41sn3aw  40920  cdleme41sn4aw  40921  cdleme41fva11  40923  cdleme42k  40930  cdleme43cN  40937  cdleme43dN  40938  cdleme46f2g1  40940  cdlemeg47rv2  40956  cdlemeg46sfg  40966  cdlemeg46fjgN  40967  cdlemeg46rjgN  40968  cdlemeg46fjv  40969  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemeg46gfv  40976  cdlemg4a  41054  cdlemg4d  41059  cdlemg4e  41060  cdlemg4f  41061  cdlemg4g  41062  cdlemg4  41063  cdlemg6d  41067  cdlemg6e  41068  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg9b  41079  cdlemg10a  41086  cdlemg10  41087  cdlemg12a  41089  cdlemg12b  41090  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg17dN  41109  cdlemg17dALTN  41110  cdlemg17e  41111  cdlemg17f  41112  cdlemg17g  41113  cdlemg17h  41114  cdlemg17i  41115  cdlemg17pq  41118  cdlemg17iqN  41120  cdlemg17  41123  cdlemg18b  41125  cdlemg18c  41126  cdlemg19a  41129  cdlemg19  41130  cdlemg28a  41139  cdlemg27b  41142  cdlemg28b  41149  cdlemg28  41150  cdlemg33a  41152  cdlemg33b  41153  cdlemg33c  41154  cdlemg33d  41155  cdlemg33e  41156  cdlemg33  41157  cdlemg35  41159  cdlemg36  41160  cdlemg44a  41177  cdlemh  41263  cdlemi2  41265  cdlemj1  41267  tendocan  41270  cdlemk5a  41281  cdlemki  41287  cdlemkvcl  41288  cdlemk10  41289  cdlemksv2  41293  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk16a  41302  cdlemk16  41303  cdlemk17  41304  cdlemk18  41314  cdlemk19  41315  cdlemkoatnle-2N  41321  cdlemk13-2N  41322  cdlemkole-2N  41323  cdlemk14-2N  41324  cdlemk15-2N  41325  cdlemk16-2N  41326  cdlemk17-2N  41327  cdlemk18-2N  41332  cdlemk19-2N  41333  cdlemk30  41340  cdlemk18-3N  41346  cdlemk23-3  41348  cdlemk25-3  41350  cdlemk27-3  41353  cdlemk37  41360  cdlemkfid1N  41367  cdlemkid1  41368  cdlemky  41372  cdlemk11ta  41375  cdlemk47  41395  cdlemk48  41396  cdlemk49  41397  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemk53a  41401  cdlemk54  41404  cdlemk39u1  41413  cdlemk19u1  41415  cdleml1N  41422  cdleml2N  41423  cdleml3N  41424  dia2dimlem6  41515  cdlemn2  41641  cdlemn2a  41642  cdlemn5pre  41646  cdlemn10  41652  cdlemn11c  41655  cdlemn11pre  41656  dihjustlem  41662  dihjust  41663  lclkrlem2y  41977  aks6d1c1  42555  relexpmulnn  44136  ormkglobd  47305  natglobalincr  47307  lincreslvec3  48958  iscnrm3llem1  49424  iscnrm3l  49426  swapffunc  49757  fucofunc  49834  amgmwlem  50277