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  8510  cofsmo  10182  axdc4lem  10368  0catg  17645  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  mulgdirlem  19072  ogrpsub  20103  ogrpaddlt  20104  ogrpsublt  20108  mdetunilem4  22590  mdetuni0  22596  mdetmul  22598  prdsxmetlem  24343  isosctrlem3  26797  isosctr  26798  amgmlem  26967  nosupbnd2lem1  27693  addsass  28011  f1otrg  28953  colinearalg  28993  ax5seglem6  29017  ax5seg  29021  axpasch  29024  axeuclidlem  29045  axeuclid  29046  uhgr2edg  29291  numclwlk1lem2  30455  rhmdvd  33399  bnj1128  35148  mclspps  35782  cgrtr  36190  cgrtr3  36192  ofscom  36205  segconeq  36208  ifscgr  36242  btwnxfr  36254  colinearxfr  36273  lineext  36274  brofs2  36275  brifs2  36276  fscgr  36278  linecgr  36279  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  seglecgr12im  36308  seglecgr12  36309  segletr  36312  broutsideof3  36324  outsideofeq  36328  lineunray  36345  lineelsb2  36346  linecom  36348  lshpkrlem5  39574  omlmod1i2N  39720  cvrnbtwn3  39736  cvrcmp  39743  cvrcmp2  39744  cvlexch2  39789  cvlexchb2  39791  cvlatexchb2  39795  cvlatexch2  39797  cvlatexch3  39798  cvlsupr7  39808  atnlej1  39839  atnlej2  39840  2llnneN  39869  cvratlem  39881  atcvrneN  39890  atcvrj1  39891  atlelt  39898  2atjm  39905  3noncolr2  39909  3noncolr1N  39910  3dimlem2  39919  3dim1  39927  3dim2  39928  1cvrat  39936  ps-1  39937  ps-2  39938  2atjlej  39939  hlatexch3N  39940  ps-2b  39942  3atlem1  39943  3atlem2  39944  3atlem5  39947  3atlem6  39948  llnle  39978  2atm  39987  ps-2c  39988  lplni2  39997  lplnle  40000  lplnnle2at  40001  lplnri3N  40015  llncvrlpln2  40017  2atmat  40021  2llnm2N  40028  2llnm4  40030  2llnmeqat  40031  lvolnle3at  40042  4atlem0ae  40054  4atlem0be  40055  4atlem3b  40058  4atlem9  40063  4atlem10a  40064  4atlem10  40066  4atlem11a  40067  4atlem12a  40070  4at2  40074  2lplnm2N  40081  lneq2at  40238  2llnma1b  40246  2llnma1  40247  2llnma3r  40248  2llnma2  40249  2llnma2rN  40250  cdlema1N  40251  paddasslem2  40281  paddasslem15  40294  paddasslem16  40295  pmodlem1  40306  pmodlem2  40307  pmod2iN  40309  hlmod1i  40316  atmod1i1m  40318  atmod2i1  40321  atmod2i2  40322  atmod3i1  40324  atmod3i2  40325  atmod4i1  40326  atmod4i2  40327  llnexchb2lem  40328  llnexch2N  40330  dalawlem3  40333  dalawlem4  40334  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem9  40339  dalawlem11  40341  dalawlem12  40342  dalawlem13  40343  dalawlem15  40345  osumcllem9N  40424  pl42lem1N  40439  4atexlems  40512  4atex2  40537  4atex2-0bOLDN  40539  trlval4  40648  cdlemc5  40655  cdlemc6  40656  cdlemd2  40659  cdlemd4  40661  cdlemd6  40663  cdleme00a  40669  cdleme0e  40677  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme4a  40699  cdleme5  40700  cdleme9  40713  cdleme16aN  40719  cdleme11c  40721  cdleme11e  40723  cdleme11g  40725  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme11l  40729  cdleme11  40730  cdleme12  40731  cdleme14  40733  cdleme15c  40736  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme0nex  40750  cdleme18a  40751  cdleme18c  40753  cdleme18d  40755  cdlemednpq  40759  cdlemednuN  40760  cdleme20zN  40761  cdleme20y  40762  cdleme19a  40763  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20aN  40769  cdleme20bN  40770  cdleme20c  40771  cdleme20d  40772  cdleme20f  40774  cdleme20g  40775  cdleme20i  40777  cdleme20j  40778  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21b  40786  cdleme21c  40787  cdleme21e  40791  cdleme21f  40792  cdleme22a  40800  cdleme22b  40801  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme26eALTN  40821  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme30a  40838  cdleme43fsv1snlem  40880  cdlemefs31fv1  40884  cdlemefs45eN  40891  cdleme32b  40902  cdleme32c  40903  cdleme32d  40904  cdleme35h  40916  cdleme36a  40920  cdleme36m  40921  cdleme37m  40922  cdleme40m  40927  cdleme40n  40928  cdleme41sn3aw  40934  cdleme41sn4aw  40935  cdleme41fva11  40937  cdleme42k  40944  cdleme43cN  40951  cdleme43dN  40952  cdleme46f2g1  40954  cdlemeg47rv2  40970  cdlemeg46sfg  40980  cdlemeg46fjgN  40981  cdlemeg46rjgN  40982  cdlemeg46fjv  40983  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdlemg4a  41068  cdlemg4d  41073  cdlemg4e  41074  cdlemg4f  41075  cdlemg4g  41076  cdlemg4  41077  cdlemg6d  41081  cdlemg6e  41082  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg10a  41100  cdlemg10  41101  cdlemg12a  41103  cdlemg12b  41104  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg17dN  41123  cdlemg17dALTN  41124  cdlemg17e  41125  cdlemg17f  41126  cdlemg17g  41127  cdlemg17h  41128  cdlemg17i  41129  cdlemg17pq  41132  cdlemg17iqN  41134  cdlemg17  41137  cdlemg18b  41139  cdlemg18c  41140  cdlemg19a  41143  cdlemg19  41144  cdlemg28a  41153  cdlemg27b  41156  cdlemg28b  41163  cdlemg28  41164  cdlemg33a  41166  cdlemg33b  41167  cdlemg33c  41168  cdlemg33d  41169  cdlemg33e  41170  cdlemg33  41171  cdlemg35  41173  cdlemg36  41174  cdlemg44a  41191  cdlemh  41277  cdlemi2  41279  cdlemj1  41281  tendocan  41284  cdlemk5a  41295  cdlemki  41301  cdlemkvcl  41302  cdlemk10  41303  cdlemksv2  41307  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk16a  41316  cdlemk16  41317  cdlemk17  41318  cdlemk18  41328  cdlemk19  41329  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk30  41354  cdlemk18-3N  41360  cdlemk23-3  41362  cdlemk25-3  41364  cdlemk27-3  41367  cdlemk37  41374  cdlemkfid1N  41381  cdlemkid1  41382  cdlemky  41386  cdlemk11ta  41389  cdlemk47  41409  cdlemk48  41410  cdlemk49  41411  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdlemk54  41418  cdlemk39u1  41427  cdlemk19u1  41429  cdleml1N  41436  cdleml2N  41437  cdleml3N  41438  dia2dimlem6  41529  cdlemn2  41655  cdlemn2a  41656  cdlemn5pre  41660  cdlemn10  41666  cdlemn11c  41669  cdlemn11pre  41670  dihjustlem  41676  dihjust  41677  lclkrlem2y  41991  aks6d1c1  42569  relexpmulnn  44154  ormkglobd  47321  natglobalincr  47323  lincreslvec3  48970  iscnrm3llem1  49436  iscnrm3l  49438  swapffunc  49769  fucofunc  49846  amgmwlem  50289