Theorem simp22 1209

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp22	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simp22

Step	Hyp	Ref	Expression
1		simp2 1138	. 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:  simp122  1308  simp222  1317  simp322  1326  elfiun  9336  cofsmo  10182  modexp  14191  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  mulgdirlem  19072  pmtrprfv3  19420  ogrpsub  20103  ogrpaddlt  20104  ogrpsublt  20108  mdetunilem4  22590  mdetuni0  22596  mdetmul  22598  prdsxmetlem  24343  isosctrlem3  26797  isosctr  26798  amgmlem  26967  f1otrg  28953  colinearalg  28993  ax5seglem6  29017  ax5seg  29021  axpasch  29024  axeuclidlem  29045  axeuclid  29046  rhmdvd  33399  bnj966  35102  mclspps  35782  cgrtr  36190  cgrtr3  36192  ofscom  36205  cgrextend  36206  btwnxfr  36254  colinearxfr  36273  lineext  36274  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  linecom  36348  eqlkr  39559  lshpkrlem5  39574  omlmod1i2N  39720  cvrnbtwn3  39736  cvrcmp2  39744  cvlexch2  39789  cvlexchb2  39791  cvlatexchb2  39795  cvlatexch1  39796  cvlatexch2  39797  cvlatexch3  39798  cvlsupr7  39808  cvlsupr8  39809  atnlej1  39839  atnlej2  39840  2llnneN  39869  cvratlem  39881  atcvrneN  39890  atlelt  39898  2atjm  39905  3noncolr2  39909  3noncolr1N  39910  hlatcon2  39912  3dimlem2  39919  3dim1  39927  3dim2  39928  1cvrat  39936  ps-1  39937  ps-2  39938  2atjlej  39939  hlatexch3N  39940  ps-2b  39942  3atlem1  39943  3atlem5  39947  3atlem6  39948  2atm  39987  ps-2c  39988  lplni2  39997  lplnri3N  40015  llncvrlpln2  40017  2atmat  40021  2llnm2N  40028  2llnm3N  40029  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  paddasslem16  40295  pmodlem1  40306  pmod2iN  40309  hlmod1i  40316  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  osumcllem7N  40422  osumcllem9N  40424  pl42lem1N  40439  4atexlemswapqr  40523  4atex2  40537  4atex2-0bOLDN  40539  trlval4  40648  cdlemc5  40655  cdlemc6  40656  cdlemd2  40659  cdlemd4  40661  cdlemd6  40663  cdleme00a  40669  cdleme0e  40677  cdleme4  40698  cdleme4a  40699  cdleme5  40700  cdleme9  40713  cdleme16aN  40719  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11g  40725  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme11l  40729  cdleme11  40730  cdleme12  40731  cdleme13  40732  cdleme14  40733  cdleme15a  40734  cdleme15c  40736  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme17d1  40749  cdleme0nex  40750  cdleme18a  40751  cdleme18b  40752  cdleme18c  40753  cdleme18d  40755  cdlemednpq  40759  cdlemednuN  40760  cdleme20zN  40761  cdleme20y  40762  cdleme19a  40763  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20aN  40769  cdleme20d  40772  cdleme20f  40774  cdleme20g  40775  cdleme20i  40777  cdleme20j  40778  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21b  40786  cdleme21c  40787  cdleme21e  40791  cdleme21j  40796  cdleme22aa  40799  cdleme22a  40800  cdleme22b  40801  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme30a  40838  cdlemefs31fv1  40884  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35h  40916  cdleme36a  40920  cdleme36m  40921  cdleme41sn3aw  40934  cdleme41sn4aw  40935  cdleme41fva11  40937  cdleme42k  40944  cdleme43cN  40951  cdleme46f2g1  40954  cdlemeg46fjgN  40981  cdlemeg46fjv  40983  cdlemeg46frv  40985  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme50trn2a  41010  cdlemg4a  41068  cdlemg4d  41073  cdlemg4e  41074  cdlemg4f  41075  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg10a  41100  cdlemg10  41101  cdlemg12b  41104  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg17dN  41123  cdlemg17dALTN  41124  cdlemg17e  41125  cdlemg17f  41126  cdlemg17g  41127  cdlemg17i  41129  cdlemg17ir  41130  cdlemg17pq  41132  cdlemg17bq  41133  cdlemg17iqN  41134  cdlemg17  41137  cdlemg18b  41139  cdlemg18c  41140  cdlemg18d  41141  cdlemg18  41142  cdlemg19  41144  cdlemg21  41146  cdlemg28a  41153  cdlemg31b0a  41155  cdlemg27b  41156  cdlemg33b0  41161  cdlemg28b  41163  cdlemg28  41164  cdlemg35  41173  cdlemg36  41174  cdlemg44a  41191  cdlemh  41277  cdlemi2  41279  cdlemj1  41281  tendocan  41284  cdlemk5a  41295  cdlemk5  41296  cdlemki  41301  cdlemkvcl  41302  cdlemk10  41303  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemkoatnle  41311  cdlemk15  41315  cdlemk16a  41316  cdlemk16  41317  cdlemk1u  41319  cdlemk5u  41321  cdlemk6u  41322  cdlemk18  41328  cdlemk19  41329  cdlemk7u  41330  cdlemk11u  41331  cdlemk12u  41332  cdlemk21N  41333  cdlemk20  41334  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  cdlemk22  41353  cdlemk30  41354  cdlemkuel-3  41358  cdlemkuv2-3N  41359  cdlemk18-3N  41360  cdlemkfid1N  41381  cdlemkid1  41382  cdlemkfid3N  41385  cdlemky  41386  cdlemk11ta  41389  cdlemk47  41409  cdlemk48  41410  cdlemk49  41411  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdlemk53  41417  cdlemk54  41418  cdlemk55a  41419  cdlemkyyN  41422  cdlemk43N  41423  cdlemk55u1  41425  cdlemk55u  41426  cdlemk39u1  41427  cdlemk19u1  41429  cdleml1N  41436  cdleml2N  41437  cdleml3N  41438  dia2dimlem6  41529  cdlemn2  41655  cdlemn2a  41656  cdlemn5pre  41660  cdlemn11a  41667  dihjustlem  41676  dihjust  41677  dihmeetlem15N  41781  lclkrlem2y  41991  aks6d1c1  42569  relexpmulnn  44154  ormkglobd  47321  natglobalincr  47323  iscnrm3llem1  49436  iscnrm3l  49438  swapffunc  49769  fucofunc  49846  amgmwlem  50289