Theorem simp22 1208

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  1307  simp222  1316  simp322  1325  elfiun  9470  cofsmo  10309  modexp  14277  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  mulgdirlem  19123  pmtrprfv3  19472  mdetunilem4  22621  mdetuni0  22627  mdetmul  22629  prdsxmetlem  24378  isosctrlem3  26863  isosctr  26864  amgmlem  27033  f1otrg  28879  colinearalg  28925  ax5seglem6  28949  ax5seg  28953  axpasch  28956  axeuclidlem  28977  axeuclid  28978  ogrpsub  33093  ogrpaddlt  33094  ogrpsublt  33098  rhmdvd  33348  bnj966  34958  mclspps  35589  cgrtr  35993  cgrtr3  35995  ofscom  36008  cgrextend  36009  btwnxfr  36057  colinearxfr  36076  lineext  36077  fscgr  36081  linecgr  36082  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  seglecgr12im  36111  seglecgr12  36112  segletr  36115  broutsideof3  36127  outsideofeq  36131  lineunray  36148  linecom  36151  eqlkr  39100  lshpkrlem5  39115  omlmod1i2N  39261  cvrnbtwn3  39277  cvrcmp2  39285  cvlexch2  39330  cvlexchb2  39332  cvlatexchb2  39336  cvlatexch1  39337  cvlatexch2  39338  cvlatexch3  39339  cvlsupr7  39349  cvlsupr8  39350  atnlej1  39381  atnlej2  39382  2llnneN  39411  cvratlem  39423  atcvrneN  39432  atlelt  39440  2atjm  39447  3noncolr2  39451  3noncolr1N  39452  hlatcon2  39454  3dimlem2  39461  3dim1  39469  3dim2  39470  1cvrat  39478  ps-1  39479  ps-2  39480  2atjlej  39481  hlatexch3N  39482  ps-2b  39484  3atlem1  39485  3atlem5  39489  3atlem6  39490  2atm  39529  ps-2c  39530  lplni2  39539  lplnri3N  39557  llncvrlpln2  39559  2atmat  39563  2llnm2N  39570  2llnm3N  39571  2llnm4  39572  2llnmeqat  39573  lvolnle3at  39584  4atlem0ae  39596  4atlem0be  39597  4atlem3b  39600  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem12a  39612  4at2  39616  2lplnm2N  39623  lneq2at  39780  2llnma1b  39788  2llnma1  39789  2llnma3r  39790  2llnma2  39791  2llnma2rN  39792  cdlema1N  39793  paddasslem2  39823  paddasslem16  39837  pmodlem1  39848  pmod2iN  39851  hlmod1i  39858  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  atmod3i2  39867  atmod4i1  39868  atmod4i2  39869  llnexchb2lem  39870  llnexch2N  39872  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem13  39885  dalawlem15  39887  osumcllem7N  39964  osumcllem9N  39966  pl42lem1N  39981  4atexlemswapqr  40065  4atex2  40079  4atex2-0bOLDN  40081  trlval4  40190  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdlemd4  40203  cdlemd6  40205  cdleme00a  40211  cdleme0e  40219  cdleme4  40240  cdleme4a  40241  cdleme5  40242  cdleme9  40255  cdleme16aN  40261  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11g  40267  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme11l  40271  cdleme11  40272  cdleme12  40273  cdleme13  40274  cdleme14  40275  cdleme15a  40276  cdleme15c  40278  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme17d1  40291  cdleme0nex  40292  cdleme18a  40293  cdleme18b  40294  cdleme18c  40295  cdleme18d  40297  cdlemednpq  40301  cdlemednuN  40302  cdleme20zN  40303  cdleme20y  40304  cdleme19a  40305  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20aN  40311  cdleme20d  40314  cdleme20f  40316  cdleme20g  40317  cdleme20i  40319  cdleme20j  40320  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21b  40328  cdleme21c  40329  cdleme21e  40333  cdleme21j  40338  cdleme22aa  40341  cdleme22a  40342  cdleme22b  40343  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme30a  40380  cdlemefs31fv1  40426  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35h  40458  cdleme36a  40462  cdleme36m  40463  cdleme41sn3aw  40476  cdleme41sn4aw  40477  cdleme41fva11  40479  cdleme42k  40486  cdleme43cN  40493  cdleme46f2g1  40496  cdlemeg46fjgN  40523  cdlemeg46fjv  40525  cdlemeg46frv  40527  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdleme50trn2a  40552  cdlemg4a  40610  cdlemg4d  40615  cdlemg4e  40616  cdlemg4f  40617  cdlemg8c  40631  cdlemg9a  40634  cdlemg9b  40635  cdlemg10a  40642  cdlemg10  40643  cdlemg12b  40646  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg17dN  40665  cdlemg17dALTN  40666  cdlemg17e  40667  cdlemg17f  40668  cdlemg17g  40669  cdlemg17i  40671  cdlemg17ir  40672  cdlemg17pq  40674  cdlemg17bq  40675  cdlemg17iqN  40676  cdlemg17  40679  cdlemg18b  40681  cdlemg18c  40682  cdlemg18d  40683  cdlemg18  40684  cdlemg19  40686  cdlemg21  40688  cdlemg28a  40695  cdlemg31b0a  40697  cdlemg27b  40698  cdlemg33b0  40703  cdlemg28b  40705  cdlemg28  40706  cdlemg35  40715  cdlemg36  40716  cdlemg44a  40733  cdlemh  40819  cdlemi2  40821  cdlemj1  40823  tendocan  40826  cdlemk5a  40837  cdlemk5  40838  cdlemki  40843  cdlemkvcl  40844  cdlemk10  40845  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemkoatnle  40853  cdlemk15  40857  cdlemk16a  40858  cdlemk16  40859  cdlemk1u  40861  cdlemk5u  40863  cdlemk6u  40864  cdlemk18  40870  cdlemk19  40871  cdlemk7u  40872  cdlemk11u  40873  cdlemk12u  40874  cdlemk21N  40875  cdlemk20  40876  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk22  40895  cdlemk30  40896  cdlemkuel-3  40900  cdlemkuv2-3N  40901  cdlemk18-3N  40902  cdlemkfid1N  40923  cdlemkid1  40924  cdlemkfid3N  40927  cdlemky  40928  cdlemk11ta  40931  cdlemk47  40951  cdlemk48  40952  cdlemk49  40953  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk53a  40957  cdlemk53  40959  cdlemk54  40960  cdlemk55a  40961  cdlemkyyN  40964  cdlemk43N  40965  cdlemk55u1  40967  cdlemk55u  40968  cdlemk39u1  40969  cdlemk19u1  40971  cdleml1N  40978  cdleml2N  40979  cdleml3N  40980  dia2dimlem6  41071  cdlemn2  41197  cdlemn2a  41198  cdlemn5pre  41202  cdlemn11a  41209  dihjustlem  41218  dihjust  41219  dihmeetlem15N  41323  lclkrlem2y  41533  aks6d1c1  42117  relexpmulnn  43722  ormkglobd  46890  natglobalincr  46892  iscnrm3llem1  48846  iscnrm3l  48848  swapffunc  48988  fucofunc  49054  amgmwlem  49321