Theorem simp22 1206

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  simp122  1305  simp222  1314  simp322  1323  elfiun  9265  cofsmo  10104  modexp  14032  funcoppc  17664  funcres  17685  catcisolem  17899  1stfcl  17988  2ndfcl  17989  prfcl  17994  evlfcl  18014  curf1cl  18020  curfcl  18024  hofcl  18051  mulgdirlem  18807  pmtrprfv3  19135  mdetunilem4  21844  mdetuni0  21850  mdetmul  21852  prdsxmetlem  23601  isosctrlem3  26050  isosctr  26051  amgmlem  26219  f1otrg  27365  colinearalg  27411  ax5seglem6  27435  ax5seg  27439  axpasch  27442  axeuclidlem  27463  axeuclid  27464  ogrpsub  31473  ogrpaddlt  31474  ogrpsublt  31478  rhmdvd  31655  bnj966  33059  mclspps  33681  cgrtr  34364  cgrtr3  34366  ofscom  34379  cgrextend  34380  btwnxfr  34428  colinearxfr  34447  lineext  34448  fscgr  34452  linecgr  34453  btwnconn1lem1  34459  btwnconn1lem2  34460  btwnconn1lem3  34461  btwnconn1lem4  34462  btwnconn1lem5  34463  btwnconn1lem6  34464  btwnconn1lem7  34465  seglecgr12im  34482  seglecgr12  34483  segletr  34486  broutsideof3  34498  outsideofeq  34502  lineunray  34519  linecom  34522  eqlkr  37338  lshpkrlem5  37353  omlmod1i2N  37499  cvrnbtwn3  37515  cvrcmp2  37523  cvlexch2  37568  cvlexchb2  37570  cvlatexchb2  37574  cvlatexch1  37575  cvlatexch2  37576  cvlatexch3  37577  cvlsupr7  37587  cvlsupr8  37588  atnlej1  37619  atnlej2  37620  2llnneN  37649  cvratlem  37661  atcvrneN  37670  atlelt  37678  2atjm  37685  3noncolr2  37689  3noncolr1N  37690  hlatcon2  37692  3dimlem2  37699  3dim1  37707  3dim2  37708  1cvrat  37716  ps-1  37717  ps-2  37718  2atjlej  37719  hlatexch3N  37720  ps-2b  37722  3atlem1  37723  3atlem5  37727  3atlem6  37728  2atm  37767  ps-2c  37768  lplni2  37777  lplnri3N  37795  llncvrlpln2  37797  2atmat  37801  2llnm2N  37808  2llnm3N  37809  2llnm4  37810  2llnmeqat  37811  lvolnle3at  37822  4atlem0ae  37834  4atlem0be  37835  4atlem3b  37838  4atlem9  37843  4atlem10a  37844  4atlem10  37846  4atlem11a  37847  4atlem12a  37850  4at2  37854  2lplnm2N  37861  lneq2at  38018  2llnma1b  38026  2llnma1  38027  2llnma3r  38028  2llnma2  38029  2llnma2rN  38030  cdlema1N  38031  paddasslem2  38061  paddasslem16  38075  pmodlem1  38086  pmod2iN  38089  hlmod1i  38096  atmod2i1  38101  atmod2i2  38102  atmod3i1  38104  atmod3i2  38105  atmod4i1  38106  atmod4i2  38107  llnexchb2lem  38108  llnexch2N  38110  dalawlem3  38113  dalawlem4  38114  dalawlem5  38115  dalawlem6  38116  dalawlem7  38117  dalawlem8  38118  dalawlem9  38119  dalawlem11  38121  dalawlem12  38122  dalawlem13  38123  dalawlem15  38125  osumcllem7N  38202  osumcllem9N  38204  pl42lem1N  38219  4atexlemswapqr  38303  4atex2  38317  4atex2-0bOLDN  38319  trlval4  38428  cdlemc5  38435  cdlemc6  38436  cdlemd2  38439  cdlemd4  38441  cdlemd6  38443  cdleme00a  38449  cdleme0e  38457  cdleme4  38478  cdleme4a  38479  cdleme5  38480  cdleme9  38493  cdleme16aN  38499  cdleme11c  38501  cdleme11dN  38502  cdleme11e  38503  cdleme11g  38505  cdleme11h  38506  cdleme11j  38507  cdleme11k  38508  cdleme11l  38509  cdleme11  38510  cdleme12  38511  cdleme13  38512  cdleme14  38513  cdleme15a  38514  cdleme15c  38516  cdleme16b  38519  cdleme16c  38520  cdleme16d  38521  cdleme16e  38522  cdleme16f  38523  cdleme17d1  38529  cdleme0nex  38530  cdleme18a  38531  cdleme18b  38532  cdleme18c  38533  cdleme18d  38535  cdlemednpq  38539  cdlemednuN  38540  cdleme20zN  38541  cdleme20y  38542  cdleme19a  38543  cdleme19b  38544  cdleme19d  38546  cdleme19e  38547  cdleme20aN  38549  cdleme20d  38552  cdleme20f  38554  cdleme20g  38555  cdleme20i  38557  cdleme20j  38558  cdleme20l1  38560  cdleme20l2  38561  cdleme20l  38562  cdleme20m  38563  cdleme21b  38566  cdleme21c  38567  cdleme21e  38571  cdleme21j  38576  cdleme22aa  38579  cdleme22a  38580  cdleme22b  38581  cdleme22cN  38582  cdleme22d  38583  cdleme22e  38584  cdleme22eALTN  38585  cdleme22f  38586  cdleme26fALTN  38602  cdleme26f  38603  cdleme26f2ALTN  38604  cdleme26f2  38605  cdleme27N  38609  cdleme28a  38610  cdleme28b  38611  cdleme30a  38618  cdlemefs31fv1  38664  cdleme32b  38682  cdleme32c  38683  cdleme32e  38685  cdleme35h  38696  cdleme36a  38700  cdleme36m  38701  cdleme41sn3aw  38714  cdleme41sn4aw  38715  cdleme41fva11  38717  cdleme42k  38724  cdleme43cN  38731  cdleme46f2g1  38734  cdlemeg46fjgN  38761  cdlemeg46fjv  38763  cdlemeg46frv  38765  cdlemeg46rgv  38768  cdlemeg46req  38769  cdlemeg46gfv  38770  cdleme50trn2a  38790  cdlemg4a  38848  cdlemg4d  38853  cdlemg4e  38854  cdlemg4f  38855  cdlemg8c  38869  cdlemg9a  38872  cdlemg9b  38873  cdlemg10a  38880  cdlemg10  38881  cdlemg12b  38884  cdlemg12f  38888  cdlemg12g  38889  cdlemg12  38890  cdlemg17dN  38903  cdlemg17dALTN  38904  cdlemg17e  38905  cdlemg17f  38906  cdlemg17g  38907  cdlemg17i  38909  cdlemg17ir  38910  cdlemg17pq  38912  cdlemg17bq  38913  cdlemg17iqN  38914  cdlemg17  38917  cdlemg18b  38919  cdlemg18c  38920  cdlemg18d  38921  cdlemg18  38922  cdlemg19  38924  cdlemg21  38926  cdlemg28a  38933  cdlemg31b0a  38935  cdlemg27b  38936  cdlemg33b0  38941  cdlemg28b  38943  cdlemg28  38944  cdlemg35  38953  cdlemg36  38954  cdlemg44a  38971  cdlemh  39057  cdlemi2  39059  cdlemj1  39061  tendocan  39064  cdlemk5a  39075  cdlemk5  39076  cdlemki  39081  cdlemkvcl  39082  cdlemk10  39083  cdlemksv2  39087  cdlemk7  39088  cdlemk11  39089  cdlemk12  39090  cdlemkoatnle  39091  cdlemk15  39095  cdlemk16a  39096  cdlemk16  39097  cdlemk1u  39099  cdlemk5u  39101  cdlemk6u  39102  cdlemk18  39108  cdlemk19  39109  cdlemk7u  39110  cdlemk11u  39111  cdlemk12u  39112  cdlemk21N  39113  cdlemk20  39114  cdlemkoatnle-2N  39115  cdlemk13-2N  39116  cdlemkole-2N  39117  cdlemk14-2N  39118  cdlemk15-2N  39119  cdlemk16-2N  39120  cdlemk17-2N  39121  cdlemk18-2N  39126  cdlemk19-2N  39127  cdlemk22  39133  cdlemk30  39134  cdlemkuel-3  39138  cdlemkuv2-3N  39139  cdlemk18-3N  39140  cdlemkfid1N  39161  cdlemkid1  39162  cdlemkfid3N  39165  cdlemky  39166  cdlemk11ta  39169  cdlemk47  39189  cdlemk48  39190  cdlemk49  39191  cdlemk50  39192  cdlemk51  39193  cdlemk52  39194  cdlemk53a  39195  cdlemk53  39197  cdlemk54  39198  cdlemk55a  39199  cdlemkyyN  39202  cdlemk43N  39203  cdlemk55u1  39205  cdlemk55u  39206  cdlemk39u1  39207  cdlemk19u1  39209  cdleml1N  39216  cdleml2N  39217  cdleml3N  39218  dia2dimlem6  39309  cdlemn2  39435  cdlemn2a  39436  cdlemn5pre  39440  cdlemn11a  39447  dihjustlem  39456  dihjust  39457  dihmeetlem15N  39561  lclkrlem2y  39771  relexpmulnn  41556  iscnrm3llem1  46513  iscnrm3l  46515  amgmwlem  46776  natglobalincr  46782