Theorem simp22 1205

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp122  1304  simp222  1313  simp322  1322  elfiun  9119  cofsmo  9956  modexp  13881  funcoppc  17506  funcres  17527  catcisolem  17741  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlfcl  17856  curf1cl  17862  curfcl  17866  hofcl  17893  mulgdirlem  18649  pmtrprfv3  18977  mdetunilem4  21672  mdetuni0  21678  mdetmul  21680  prdsxmetlem  23429  isosctrlem3  25875  isosctr  25876  amgmlem  26044  f1otrg  27136  colinearalg  27181  ax5seglem6  27205  ax5seg  27209  axpasch  27212  axeuclidlem  27233  axeuclid  27234  ogrpsub  31244  ogrpaddlt  31245  ogrpsublt  31249  rhmdvd  31422  bnj966  32824  mclspps  33446  cgrtr  34221  cgrtr3  34223  ofscom  34236  cgrextend  34237  btwnxfr  34285  colinearxfr  34304  lineext  34305  fscgr  34309  linecgr  34310  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem7  34322  seglecgr12im  34339  seglecgr12  34340  segletr  34343  broutsideof3  34355  outsideofeq  34359  lineunray  34376  linecom  34379  eqlkr  37040  lshpkrlem5  37055  omlmod1i2N  37201  cvrnbtwn3  37217  cvrcmp2  37225  cvlexch2  37270  cvlexchb2  37272  cvlatexchb2  37276  cvlatexch1  37277  cvlatexch2  37278  cvlatexch3  37279  cvlsupr7  37289  cvlsupr8  37290  atnlej1  37320  atnlej2  37321  2llnneN  37350  cvratlem  37362  atcvrneN  37371  atlelt  37379  2atjm  37386  3noncolr2  37390  3noncolr1N  37391  hlatcon2  37393  3dimlem2  37400  3dim1  37408  3dim2  37409  1cvrat  37417  ps-1  37418  ps-2  37419  2atjlej  37420  hlatexch3N  37421  ps-2b  37423  3atlem1  37424  3atlem5  37428  3atlem6  37429  2atm  37468  ps-2c  37469  lplni2  37478  lplnri3N  37496  llncvrlpln2  37498  2atmat  37502  2llnm2N  37509  2llnm3N  37510  2llnm4  37511  2llnmeqat  37512  lvolnle3at  37523  4atlem0ae  37535  4atlem0be  37536  4atlem3b  37539  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem12a  37551  4at2  37555  2lplnm2N  37562  lneq2at  37719  2llnma1b  37727  2llnma1  37728  2llnma3r  37729  2llnma2  37730  2llnma2rN  37731  cdlema1N  37732  paddasslem2  37762  paddasslem16  37776  pmodlem1  37787  pmod2iN  37790  hlmod1i  37797  atmod2i1  37802  atmod2i2  37803  atmod3i1  37805  atmod3i2  37806  atmod4i1  37807  atmod4i2  37808  llnexchb2lem  37809  llnexch2N  37811  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  dalawlem13  37824  dalawlem15  37826  osumcllem7N  37903  osumcllem9N  37905  pl42lem1N  37920  4atexlemswapqr  38004  4atex2  38018  4atex2-0bOLDN  38020  trlval4  38129  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdlemd4  38142  cdlemd6  38144  cdleme00a  38150  cdleme0e  38158  cdleme4  38179  cdleme4a  38180  cdleme5  38181  cdleme9  38194  cdleme16aN  38200  cdleme11c  38202  cdleme11dN  38203  cdleme11e  38204  cdleme11g  38206  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme11l  38210  cdleme11  38211  cdleme12  38212  cdleme13  38213  cdleme14  38214  cdleme15a  38215  cdleme15c  38217  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme17d1  38230  cdleme0nex  38231  cdleme18a  38232  cdleme18b  38233  cdleme18c  38234  cdleme18d  38236  cdlemednpq  38240  cdlemednuN  38241  cdleme20zN  38242  cdleme20y  38243  cdleme19a  38244  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20aN  38250  cdleme20d  38253  cdleme20f  38255  cdleme20g  38256  cdleme20i  38258  cdleme20j  38259  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21b  38267  cdleme21c  38268  cdleme21e  38272  cdleme21j  38277  cdleme22aa  38280  cdleme22a  38281  cdleme22b  38282  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme30a  38319  cdlemefs31fv1  38365  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35h  38397  cdleme36a  38401  cdleme36m  38402  cdleme41sn3aw  38415  cdleme41sn4aw  38416  cdleme41fva11  38418  cdleme42k  38425  cdleme43cN  38432  cdleme46f2g1  38435  cdlemeg46fjgN  38462  cdlemeg46fjv  38464  cdlemeg46frv  38466  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdleme50trn2a  38491  cdlemg4a  38549  cdlemg4d  38554  cdlemg4e  38555  cdlemg4f  38556  cdlemg8c  38570  cdlemg9a  38573  cdlemg9b  38574  cdlemg10a  38581  cdlemg10  38582  cdlemg12b  38585  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg17dN  38604  cdlemg17dALTN  38605  cdlemg17e  38606  cdlemg17f  38607  cdlemg17g  38608  cdlemg17i  38610  cdlemg17ir  38611  cdlemg17pq  38613  cdlemg17bq  38614  cdlemg17iqN  38615  cdlemg17  38618  cdlemg18b  38620  cdlemg18c  38621  cdlemg18d  38622  cdlemg18  38623  cdlemg19  38625  cdlemg21  38627  cdlemg28a  38634  cdlemg31b0a  38636  cdlemg27b  38637  cdlemg33b0  38642  cdlemg28b  38644  cdlemg28  38645  cdlemg35  38654  cdlemg36  38655  cdlemg44a  38672  cdlemh  38758  cdlemi2  38760  cdlemj1  38762  tendocan  38765  cdlemk5a  38776  cdlemk5  38777  cdlemki  38782  cdlemkvcl  38783  cdlemk10  38784  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkoatnle  38792  cdlemk15  38796  cdlemk16a  38797  cdlemk16  38798  cdlemk1u  38800  cdlemk5u  38802  cdlemk6u  38803  cdlemk18  38809  cdlemk19  38810  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk21N  38814  cdlemk20  38815  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk22  38834  cdlemk30  38835  cdlemkuel-3  38839  cdlemkuv2-3N  38840  cdlemk18-3N  38841  cdlemkfid1N  38862  cdlemkid1  38863  cdlemkfid3N  38866  cdlemky  38867  cdlemk11ta  38870  cdlemk47  38890  cdlemk48  38891  cdlemk49  38892  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk53a  38896  cdlemk53  38898  cdlemk54  38899  cdlemk55a  38900  cdlemkyyN  38903  cdlemk43N  38904  cdlemk55u1  38906  cdlemk55u  38907  cdlemk39u1  38908  cdlemk19u1  38910  cdleml1N  38917  cdleml2N  38918  cdleml3N  38919  dia2dimlem6  39010  cdlemn2  39136  cdlemn2a  39137  cdlemn5pre  39141  cdlemn11a  39148  dihjustlem  39157  dihjust  39158  dihmeetlem15N  39262  lclkrlem2y  39472  relexpmulnn  41206  iscnrm3llem1  46131  iscnrm3l  46133  amgmwlem  46392