Theorem simp22 1221

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simpl22OLD  1295  simpr22OLD  1313  simp122  1362  simp222  1371  simp322  1380  elfiun  8626  cofsmo  9428  modexp  13323  funcoppc  16931  funcres  16952  catcisolem  17152  1stfcl  17234  2ndfcl  17235  prfcl  17240  evlfcl  17259  curf1cl  17265  curfcl  17269  hofcl  17296  mulgdirlem  17968  pmtrprfv3  18268  mdetunilem4  20837  mdetuni0  20843  mdetmul  20845  prdsxmetlem  22592  isosctrlem3  25009  isosctr  25010  amgmlem  25179  f1otrg  26237  colinearalg  26276  ax5seglem6  26300  ax5seg  26304  axpasch  26307  axeuclidlem  26328  axeuclid  26329  ogrpsub  30287  ogrpaddlt  30288  ogrpsublt  30292  rhmdvd  30391  bnj966  31621  mclspps  32088  cgrtr  32696  cgrtr3  32698  ofscom  32711  cgrextend  32712  btwnxfr  32760  colinearxfr  32779  lineext  32780  fscgr  32784  linecgr  32785  btwnconn1lem1  32791  btwnconn1lem2  32792  btwnconn1lem3  32793  btwnconn1lem4  32794  btwnconn1lem5  32795  btwnconn1lem6  32796  btwnconn1lem7  32797  seglecgr12im  32814  seglecgr12  32815  segletr  32818  broutsideof3  32830  outsideofeq  32834  lineunray  32851  linecom  32854  eqlkr  35262  lshpkrlem5  35277  omlmod1i2N  35423  cvrnbtwn3  35439  cvrcmp2  35447  cvlexch2  35492  cvlexchb2  35494  cvlatexchb2  35498  cvlatexch1  35499  cvlatexch2  35500  cvlatexch3  35501  cvlsupr7  35511  cvlsupr8  35512  atnlej1  35542  atnlej2  35543  2llnneN  35572  cvratlem  35584  atcvrneN  35593  atlelt  35601  2atjm  35608  3noncolr2  35612  3noncolr1N  35613  hlatcon2  35615  3dimlem2  35622  3dim1  35630  3dim2  35631  1cvrat  35639  ps-1  35640  ps-2  35641  2atjlej  35642  hlatexch3N  35643  ps-2b  35645  3atlem1  35646  3atlem5  35650  3atlem6  35651  2atm  35690  ps-2c  35691  lplni2  35700  lplnri3N  35718  llncvrlpln2  35720  2atmat  35724  2llnm2N  35731  2llnm3N  35732  2llnm4  35733  2llnmeqat  35734  lvolnle3at  35745  4atlem0ae  35757  4atlem0be  35758  4atlem3b  35761  4atlem9  35766  4atlem10a  35767  4atlem10  35769  4atlem11a  35770  4atlem12a  35773  4at2  35777  2lplnm2N  35784  lneq2at  35941  2llnma1b  35949  2llnma1  35950  2llnma3r  35951  2llnma2  35952  2llnma2rN  35953  cdlema1N  35954  paddasslem2  35984  paddasslem16  35998  pmodlem1  36009  pmod2iN  36012  hlmod1i  36019  atmod2i1  36024  atmod2i2  36025  atmod3i1  36027  atmod3i2  36028  atmod4i1  36029  atmod4i2  36030  llnexchb2lem  36031  llnexch2N  36033  dalawlem3  36036  dalawlem4  36037  dalawlem5  36038  dalawlem6  36039  dalawlem7  36040  dalawlem8  36041  dalawlem9  36042  dalawlem11  36044  dalawlem12  36045  dalawlem13  36046  dalawlem15  36048  osumcllem7N  36125  osumcllem9N  36127  pl42lem1N  36142  4atexlemswapqr  36226  4atex2  36240  4atex2-0bOLDN  36242  trlval4  36351  cdlemc5  36358  cdlemc6  36359  cdlemd2  36362  cdlemd4  36364  cdlemd6  36366  cdleme00a  36372  cdleme0e  36380  cdleme4  36401  cdleme4a  36402  cdleme5  36403  cdleme9  36416  cdleme16aN  36422  cdleme11c  36424  cdleme11dN  36425  cdleme11e  36426  cdleme11g  36428  cdleme11h  36429  cdleme11j  36430  cdleme11k  36431  cdleme11l  36432  cdleme11  36433  cdleme12  36434  cdleme13  36435  cdleme14  36436  cdleme15a  36437  cdleme15c  36439  cdleme16b  36442  cdleme16c  36443  cdleme16d  36444  cdleme16e  36445  cdleme16f  36446  cdleme17d1  36452  cdleme0nex  36453  cdleme18a  36454  cdleme18b  36455  cdleme18c  36456  cdleme18d  36458  cdlemednpq  36462  cdlemednuN  36463  cdleme20zN  36464  cdleme20y  36465  cdleme19a  36466  cdleme19b  36467  cdleme19d  36469  cdleme19e  36470  cdleme20aN  36472  cdleme20d  36475  cdleme20f  36477  cdleme20g  36478  cdleme20i  36480  cdleme20j  36481  cdleme20l1  36483  cdleme20l2  36484  cdleme20l  36485  cdleme20m  36486  cdleme21b  36489  cdleme21c  36490  cdleme21e  36494  cdleme21j  36499  cdleme22aa  36502  cdleme22a  36503  cdleme22b  36504  cdleme22cN  36505  cdleme22d  36506  cdleme22e  36507  cdleme22eALTN  36508  cdleme22f  36509  cdleme26fALTN  36525  cdleme26f  36526  cdleme26f2ALTN  36527  cdleme26f2  36528  cdleme27N  36532  cdleme28a  36533  cdleme28b  36534  cdleme30a  36541  cdlemefs31fv1  36587  cdleme32b  36605  cdleme32c  36606  cdleme32e  36608  cdleme35h  36619  cdleme36a  36623  cdleme36m  36624  cdleme41sn3aw  36637  cdleme41sn4aw  36638  cdleme41fva11  36640  cdleme42k  36647  cdleme43cN  36654  cdleme46f2g1  36657  cdlemeg46fjgN  36684  cdlemeg46fjv  36686  cdlemeg46frv  36688  cdlemeg46rgv  36691  cdlemeg46req  36692  cdlemeg46gfv  36693  cdleme50trn2a  36713  cdlemg4a  36771  cdlemg4d  36776  cdlemg4e  36777  cdlemg4f  36778  cdlemg8c  36792  cdlemg9a  36795  cdlemg9b  36796  cdlemg10a  36803  cdlemg10  36804  cdlemg12b  36807  cdlemg12f  36811  cdlemg12g  36812  cdlemg12  36813  cdlemg17dN  36826  cdlemg17dALTN  36827  cdlemg17e  36828  cdlemg17f  36829  cdlemg17g  36830  cdlemg17i  36832  cdlemg17ir  36833  cdlemg17pq  36835  cdlemg17bq  36836  cdlemg17iqN  36837  cdlemg17  36840  cdlemg18b  36842  cdlemg18c  36843  cdlemg18d  36844  cdlemg18  36845  cdlemg19  36847  cdlemg21  36849  cdlemg28a  36856  cdlemg31b0a  36858  cdlemg27b  36859  cdlemg33b0  36864  cdlemg28b  36866  cdlemg28  36867  cdlemg35  36876  cdlemg36  36877  cdlemg44a  36894  cdlemh  36980  cdlemi2  36982  cdlemj1  36984  tendocan  36987  cdlemk5a  36998  cdlemk5  36999  cdlemki  37004  cdlemkvcl  37005  cdlemk10  37006  cdlemksv2  37010  cdlemk7  37011  cdlemk11  37012  cdlemk12  37013  cdlemkoatnle  37014  cdlemk15  37018  cdlemk16a  37019  cdlemk16  37020  cdlemk1u  37022  cdlemk5u  37024  cdlemk6u  37025  cdlemk18  37031  cdlemk19  37032  cdlemk7u  37033  cdlemk11u  37034  cdlemk12u  37035  cdlemk21N  37036  cdlemk20  37037  cdlemkoatnle-2N  37038  cdlemk13-2N  37039  cdlemkole-2N  37040  cdlemk14-2N  37041  cdlemk15-2N  37042  cdlemk16-2N  37043  cdlemk17-2N  37044  cdlemk18-2N  37049  cdlemk19-2N  37050  cdlemk22  37056  cdlemk30  37057  cdlemkuel-3  37061  cdlemkuv2-3N  37062  cdlemk18-3N  37063  cdlemkfid1N  37084  cdlemkid1  37085  cdlemkfid3N  37088  cdlemky  37089  cdlemk11ta  37092  cdlemk47  37112  cdlemk48  37113  cdlemk49  37114  cdlemk50  37115  cdlemk51  37116  cdlemk52  37117  cdlemk53a  37118  cdlemk53  37120  cdlemk54  37121  cdlemk55a  37122  cdlemkyyN  37125  cdlemk43N  37126  cdlemk55u1  37128  cdlemk55u  37129  cdlemk39u1  37130  cdlemk19u1  37132  cdleml1N  37139  cdleml2N  37140  cdleml3N  37141  dia2dimlem6  37232  cdlemn2  37358  cdlemn2a  37359  cdlemn5pre  37363  cdlemn11a  37370  dihjustlem  37379  dihjust  37380  dihmeetlem15N  37484  lclkrlem2y  37694  relexpmulnn  38972  amgmwlem  43668