Theorem simp22 1204

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp122  1303  simp222  1312  simp322  1321  elfiun  9466  cofsmo  10303  modexp  14250  funcoppc  17889  funcres  17910  catcisolem  18127  1stfcl  18216  2ndfcl  18217  prfcl  18222  evlfcl  18242  curf1cl  18248  curfcl  18252  hofcl  18279  mulgdirlem  19095  pmtrprfv3  19448  mdetunilem4  22605  mdetuni0  22611  mdetmul  22613  prdsxmetlem  24362  isosctrlem3  26845  isosctr  26846  amgmlem  27015  f1otrg  28795  colinearalg  28841  ax5seglem6  28865  ax5seg  28869  axpasch  28872  axeuclidlem  28893  axeuclid  28894  ogrpsub  32955  ogrpaddlt  32956  ogrpsublt  32960  rhmdvd  33201  bnj966  34802  mclspps  35425  cgrtr  35829  cgrtr3  35831  ofscom  35844  cgrextend  35845  btwnxfr  35893  colinearxfr  35912  lineext  35913  fscgr  35917  linecgr  35918  btwnconn1lem1  35924  btwnconn1lem2  35925  btwnconn1lem3  35926  btwnconn1lem4  35927  btwnconn1lem5  35928  btwnconn1lem6  35929  btwnconn1lem7  35930  seglecgr12im  35947  seglecgr12  35948  segletr  35951  broutsideof3  35963  outsideofeq  35967  lineunray  35984  linecom  35987  eqlkr  38810  lshpkrlem5  38825  omlmod1i2N  38971  cvrnbtwn3  38987  cvrcmp2  38995  cvlexch2  39040  cvlexchb2  39042  cvlatexchb2  39046  cvlatexch1  39047  cvlatexch2  39048  cvlatexch3  39049  cvlsupr7  39059  cvlsupr8  39060  atnlej1  39091  atnlej2  39092  2llnneN  39121  cvratlem  39133  atcvrneN  39142  atlelt  39150  2atjm  39157  3noncolr2  39161  3noncolr1N  39162  hlatcon2  39164  3dimlem2  39171  3dim1  39179  3dim2  39180  1cvrat  39188  ps-1  39189  ps-2  39190  2atjlej  39191  hlatexch3N  39192  ps-2b  39194  3atlem1  39195  3atlem5  39199  3atlem6  39200  2atm  39239  ps-2c  39240  lplni2  39249  lplnri3N  39267  llncvrlpln2  39269  2atmat  39273  2llnm2N  39280  2llnm3N  39281  2llnm4  39282  2llnmeqat  39283  lvolnle3at  39294  4atlem0ae  39306  4atlem0be  39307  4atlem3b  39310  4atlem9  39315  4atlem10a  39316  4atlem10  39318  4atlem11a  39319  4atlem12a  39322  4at2  39326  2lplnm2N  39333  lneq2at  39490  2llnma1b  39498  2llnma1  39499  2llnma3r  39500  2llnma2  39501  2llnma2rN  39502  cdlema1N  39503  paddasslem2  39533  paddasslem16  39547  pmodlem1  39558  pmod2iN  39561  hlmod1i  39568  atmod2i1  39573  atmod2i2  39574  atmod3i1  39576  atmod3i2  39577  atmod4i1  39578  atmod4i2  39579  llnexchb2lem  39580  llnexch2N  39582  dalawlem3  39585  dalawlem4  39586  dalawlem5  39587  dalawlem6  39588  dalawlem7  39589  dalawlem8  39590  dalawlem9  39591  dalawlem11  39593  dalawlem12  39594  dalawlem13  39595  dalawlem15  39597  osumcllem7N  39674  osumcllem9N  39676  pl42lem1N  39691  4atexlemswapqr  39775  4atex2  39789  4atex2-0bOLDN  39791  trlval4  39900  cdlemc5  39907  cdlemc6  39908  cdlemd2  39911  cdlemd4  39913  cdlemd6  39915  cdleme00a  39921  cdleme0e  39929  cdleme4  39950  cdleme4a  39951  cdleme5  39952  cdleme9  39965  cdleme16aN  39971  cdleme11c  39973  cdleme11dN  39974  cdleme11e  39975  cdleme11g  39977  cdleme11h  39978  cdleme11j  39979  cdleme11k  39980  cdleme11l  39981  cdleme11  39982  cdleme12  39983  cdleme13  39984  cdleme14  39985  cdleme15a  39986  cdleme15c  39988  cdleme16b  39991  cdleme16c  39992  cdleme16d  39993  cdleme16e  39994  cdleme16f  39995  cdleme17d1  40001  cdleme0nex  40002  cdleme18a  40003  cdleme18b  40004  cdleme18c  40005  cdleme18d  40007  cdlemednpq  40011  cdlemednuN  40012  cdleme20zN  40013  cdleme20y  40014  cdleme19a  40015  cdleme19b  40016  cdleme19d  40018  cdleme19e  40019  cdleme20aN  40021  cdleme20d  40024  cdleme20f  40026  cdleme20g  40027  cdleme20i  40029  cdleme20j  40030  cdleme20l1  40032  cdleme20l2  40033  cdleme20l  40034  cdleme20m  40035  cdleme21b  40038  cdleme21c  40039  cdleme21e  40043  cdleme21j  40048  cdleme22aa  40051  cdleme22a  40052  cdleme22b  40053  cdleme22cN  40054  cdleme22d  40055  cdleme22e  40056  cdleme22eALTN  40057  cdleme22f  40058  cdleme26fALTN  40074  cdleme26f  40075  cdleme26f2ALTN  40076  cdleme26f2  40077  cdleme27N  40081  cdleme28a  40082  cdleme28b  40083  cdleme30a  40090  cdlemefs31fv1  40136  cdleme32b  40154  cdleme32c  40155  cdleme32e  40157  cdleme35h  40168  cdleme36a  40172  cdleme36m  40173  cdleme41sn3aw  40186  cdleme41sn4aw  40187  cdleme41fva11  40189  cdleme42k  40196  cdleme43cN  40203  cdleme46f2g1  40206  cdlemeg46fjgN  40233  cdlemeg46fjv  40235  cdlemeg46frv  40237  cdlemeg46rgv  40240  cdlemeg46req  40241  cdlemeg46gfv  40242  cdleme50trn2a  40262  cdlemg4a  40320  cdlemg4d  40325  cdlemg4e  40326  cdlemg4f  40327  cdlemg8c  40341  cdlemg9a  40344  cdlemg9b  40345  cdlemg10a  40352  cdlemg10  40353  cdlemg12b  40356  cdlemg12f  40360  cdlemg12g  40361  cdlemg12  40362  cdlemg17dN  40375  cdlemg17dALTN  40376  cdlemg17e  40377  cdlemg17f  40378  cdlemg17g  40379  cdlemg17i  40381  cdlemg17ir  40382  cdlemg17pq  40384  cdlemg17bq  40385  cdlemg17iqN  40386  cdlemg17  40389  cdlemg18b  40391  cdlemg18c  40392  cdlemg18d  40393  cdlemg18  40394  cdlemg19  40396  cdlemg21  40398  cdlemg28a  40405  cdlemg31b0a  40407  cdlemg27b  40408  cdlemg33b0  40413  cdlemg28b  40415  cdlemg28  40416  cdlemg35  40425  cdlemg36  40426  cdlemg44a  40443  cdlemh  40529  cdlemi2  40531  cdlemj1  40533  tendocan  40536  cdlemk5a  40547  cdlemk5  40548  cdlemki  40553  cdlemkvcl  40554  cdlemk10  40555  cdlemksv2  40559  cdlemk7  40560  cdlemk11  40561  cdlemk12  40562  cdlemkoatnle  40563  cdlemk15  40567  cdlemk16a  40568  cdlemk16  40569  cdlemk1u  40571  cdlemk5u  40573  cdlemk6u  40574  cdlemk18  40580  cdlemk19  40581  cdlemk7u  40582  cdlemk11u  40583  cdlemk12u  40584  cdlemk21N  40585  cdlemk20  40586  cdlemkoatnle-2N  40587  cdlemk13-2N  40588  cdlemkole-2N  40589  cdlemk14-2N  40590  cdlemk15-2N  40591  cdlemk16-2N  40592  cdlemk17-2N  40593  cdlemk18-2N  40598  cdlemk19-2N  40599  cdlemk22  40605  cdlemk30  40606  cdlemkuel-3  40610  cdlemkuv2-3N  40611  cdlemk18-3N  40612  cdlemkfid1N  40633  cdlemkid1  40634  cdlemkfid3N  40637  cdlemky  40638  cdlemk11ta  40641  cdlemk47  40661  cdlemk48  40662  cdlemk49  40663  cdlemk50  40664  cdlemk51  40665  cdlemk52  40666  cdlemk53a  40667  cdlemk53  40669  cdlemk54  40670  cdlemk55a  40671  cdlemkyyN  40674  cdlemk43N  40675  cdlemk55u1  40677  cdlemk55u  40678  cdlemk39u1  40679  cdlemk19u1  40681  cdleml1N  40688  cdleml2N  40689  cdleml3N  40690  dia2dimlem6  40781  cdlemn2  40907  cdlemn2a  40908  cdlemn5pre  40912  cdlemn11a  40919  dihjustlem  40928  dihjust  40929  dihmeetlem15N  41033  lclkrlem2y  41243  aks6d1c1  41828  relexpmulnn  43413  natglobalincr  46532  iscnrm3llem1  48319  iscnrm3l  48321  amgmwlem  48586