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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp122  1303  simp222  1312  simp322  1321  elfiun  8878  cofsmo  9680  modexp  13595  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  mulgdirlem  18250  pmtrprfv3  18574  mdetunilem4  21220  mdetuni0  21226  mdetmul  21228  prdsxmetlem  22975  isosctrlem3  25406  isosctr  25407  amgmlem  25575  f1otrg  26665  colinearalg  26704  ax5seglem6  26728  ax5seg  26732  axpasch  26735  axeuclidlem  26756  axeuclid  26757  ogrpsub  30767  ogrpaddlt  30768  ogrpsublt  30772  rhmdvd  30945  bnj966  32326  mclspps  32944  cgrtr  33566  cgrtr3  33568  ofscom  33581  cgrextend  33582  btwnxfr  33630  colinearxfr  33649  lineext  33650  fscgr  33654  linecgr  33655  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem7  33667  seglecgr12im  33684  seglecgr12  33685  segletr  33688  broutsideof3  33700  outsideofeq  33704  lineunray  33721  linecom  33724  eqlkr  36395  lshpkrlem5  36410  omlmod1i2N  36556  cvrnbtwn3  36572  cvrcmp2  36580  cvlexch2  36625  cvlexchb2  36627  cvlatexchb2  36631  cvlatexch1  36632  cvlatexch2  36633  cvlatexch3  36634  cvlsupr7  36644  cvlsupr8  36645  atnlej1  36675  atnlej2  36676  2llnneN  36705  cvratlem  36717  atcvrneN  36726  atlelt  36734  2atjm  36741  3noncolr2  36745  3noncolr1N  36746  hlatcon2  36748  3dimlem2  36755  3dim1  36763  3dim2  36764  1cvrat  36772  ps-1  36773  ps-2  36774  2atjlej  36775  hlatexch3N  36776  ps-2b  36778  3atlem1  36779  3atlem5  36783  3atlem6  36784  2atm  36823  ps-2c  36824  lplni2  36833  lplnri3N  36851  llncvrlpln2  36853  2atmat  36857  2llnm2N  36864  2llnm3N  36865  2llnm4  36866  2llnmeqat  36867  lvolnle3at  36878  4atlem0ae  36890  4atlem0be  36891  4atlem3b  36894  4atlem9  36899  4atlem10a  36900  4atlem10  36902  4atlem11a  36903  4atlem12a  36906  4at2  36910  2lplnm2N  36917  lneq2at  37074  2llnma1b  37082  2llnma1  37083  2llnma3r  37084  2llnma2  37085  2llnma2rN  37086  cdlema1N  37087  paddasslem2  37117  paddasslem16  37131  pmodlem1  37142  pmod2iN  37145  hlmod1i  37152  atmod2i1  37157  atmod2i2  37158  atmod3i1  37160  atmod3i2  37161  atmod4i1  37162  atmod4i2  37163  llnexchb2lem  37164  llnexch2N  37166  dalawlem3  37169  dalawlem4  37170  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem9  37175  dalawlem11  37177  dalawlem12  37178  dalawlem13  37179  dalawlem15  37181  osumcllem7N  37258  osumcllem9N  37260  pl42lem1N  37275  4atexlemswapqr  37359  4atex2  37373  4atex2-0bOLDN  37375  trlval4  37484  cdlemc5  37491  cdlemc6  37492  cdlemd2  37495  cdlemd4  37497  cdlemd6  37499  cdleme00a  37505  cdleme0e  37513  cdleme4  37534  cdleme4a  37535  cdleme5  37536  cdleme9  37549  cdleme16aN  37555  cdleme11c  37557  cdleme11dN  37558  cdleme11e  37559  cdleme11g  37561  cdleme11h  37562  cdleme11j  37563  cdleme11k  37564  cdleme11l  37565  cdleme11  37566  cdleme12  37567  cdleme13  37568  cdleme14  37569  cdleme15a  37570  cdleme15c  37572  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme16e  37578  cdleme16f  37579  cdleme17d1  37585  cdleme0nex  37586  cdleme18a  37587  cdleme18b  37588  cdleme18c  37589  cdleme18d  37591  cdlemednpq  37595  cdlemednuN  37596  cdleme20zN  37597  cdleme20y  37598  cdleme19a  37599  cdleme19b  37600  cdleme19d  37602  cdleme19e  37603  cdleme20aN  37605  cdleme20d  37608  cdleme20f  37610  cdleme20g  37611  cdleme20i  37613  cdleme20j  37614  cdleme20l1  37616  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme21b  37622  cdleme21c  37623  cdleme21e  37627  cdleme21j  37632  cdleme22aa  37635  cdleme22a  37636  cdleme22b  37637  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme27N  37665  cdleme28a  37666  cdleme28b  37667  cdleme30a  37674  cdlemefs31fv1  37720  cdleme32b  37738  cdleme32c  37739  cdleme32e  37741  cdleme35h  37752  cdleme36a  37756  cdleme36m  37757  cdleme41sn3aw  37770  cdleme41sn4aw  37771  cdleme41fva11  37773  cdleme42k  37780  cdleme43cN  37787  cdleme46f2g1  37790  cdlemeg46fjgN  37817  cdlemeg46fjv  37819  cdlemeg46frv  37821  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme50trn2a  37846  cdlemg4a  37904  cdlemg4d  37909  cdlemg4e  37910  cdlemg4f  37911  cdlemg8c  37925  cdlemg9a  37928  cdlemg9b  37929  cdlemg10a  37936  cdlemg10  37937  cdlemg12b  37940  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg17dN  37959  cdlemg17dALTN  37960  cdlemg17e  37961  cdlemg17f  37962  cdlemg17g  37963  cdlemg17i  37965  cdlemg17ir  37966  cdlemg17pq  37968  cdlemg17bq  37969  cdlemg17iqN  37970  cdlemg17  37973  cdlemg18b  37975  cdlemg18c  37976  cdlemg18d  37977  cdlemg18  37978  cdlemg19  37980  cdlemg21  37982  cdlemg28a  37989  cdlemg31b0a  37991  cdlemg27b  37992  cdlemg33b0  37997  cdlemg28b  37999  cdlemg28  38000  cdlemg35  38009  cdlemg36  38010  cdlemg44a  38027  cdlemh  38113  cdlemi2  38115  cdlemj1  38117  tendocan  38120  cdlemk5a  38131  cdlemk5  38132  cdlemki  38137  cdlemkvcl  38138  cdlemk10  38139  cdlemksv2  38143  cdlemk7  38144  cdlemk11  38145  cdlemk12  38146  cdlemkoatnle  38147  cdlemk15  38151  cdlemk16a  38152  cdlemk16  38153  cdlemk1u  38155  cdlemk5u  38157  cdlemk6u  38158  cdlemk18  38164  cdlemk19  38165  cdlemk7u  38166  cdlemk11u  38167  cdlemk12u  38168  cdlemk21N  38169  cdlemk20  38170  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk22  38189  cdlemk30  38190  cdlemkuel-3  38194  cdlemkuv2-3N  38195  cdlemk18-3N  38196  cdlemkfid1N  38217  cdlemkid1  38218  cdlemkfid3N  38221  cdlemky  38222  cdlemk11ta  38225  cdlemk47  38245  cdlemk48  38246  cdlemk49  38247  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  cdlemk53a  38251  cdlemk53  38253  cdlemk54  38254  cdlemk55a  38255  cdlemkyyN  38258  cdlemk43N  38259  cdlemk55u1  38261  cdlemk55u  38262  cdlemk39u1  38263  cdlemk19u1  38265  cdleml1N  38272  cdleml2N  38273  cdleml3N  38274  dia2dimlem6  38365  cdlemn2  38491  cdlemn2a  38492  cdlemn5pre  38496  cdlemn11a  38503  dihjustlem  38512  dihjust  38513  dihmeetlem15N  38617  lclkrlem2y  38827  relexpmulnn  40410  amgmwlem  45330