Theorem simp22 1226

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp122  1325  simp222  1334  simp322  1343  elfiun  9415  cofsmo  10340  modexp  14375  funcoppc  18043  funcres  18064  catcisolem  18278  1stfcl  18364  2ndfcl  18365  prfcl  18370  evlfcl  18389  curf1cl  18395  curfcl  18399  hofcl  18426  mulgdirlem  19308  pmtrprfv3  19661  ogrpsub  20344  ogrpaddlt  20345  ogrpsublt  20349  mdetunilem4  22923  mdetuni0  22929  mdetmul  22931  prdsxmetlem  24680  isosctrlem3  27141  isosctr  27142  amgmlem  27310  f1otrg  29441  colinearalg  29481  ax5seglem6  29505  ax5seg  29509  axpasch  29512  axeuclidlem  29533  axeuclid  29534  rhmdvd  33878  bnj966  35567  mclspps  36328  cgrtr  36737  cgrtr3  36739  ofscom  36752  cgrextend  36753  btwnxfr  36801  colinearxfr  36820  lineext  36821  fscgr  36825  linecgr  36826  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem3  36834  btwnconn1lem4  36835  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem7  36838  seglecgr12im  36855  seglecgr12  36856  segletr  36859  broutsideof3  36871  outsideofeq  36875  lineunray  36892  linecom  36895  eqlkr  40136  lshpkrlem5  40151  omlmod1i2N  40297  cvrnbtwn3  40313  cvrcmp2  40321  cvlexch2  40366  cvlexchb2  40368  cvlatexchb2  40372  cvlatexch1  40373  cvlatexch2  40374  cvlatexch3  40375  cvlsupr7  40385  cvlsupr8  40386  atnlej1  40416  atnlej2  40417  2llnneN  40446  cvratlem  40458  atcvrneN  40467  atlelt  40475  2atjm  40482  3noncolr2  40486  3noncolr1N  40487  hlatcon2  40489  3dimlem2  40496  3dim1  40504  3dim2  40505  1cvrat  40513  ps-1  40514  ps-2  40515  2atjlej  40516  hlatexch3N  40517  ps-2b  40519  3atlem1  40520  3atlem5  40524  3atlem6  40525  2atm  40564  ps-2c  40565  lplni2  40574  lplnri3N  40592  llncvrlpln2  40594  2atmat  40598  2llnm2N  40605  2llnm3N  40606  2llnm4  40607  2llnmeqat  40608  lvolnle3at  40619  4atlem0ae  40631  4atlem0be  40632  4atlem3b  40635  4atlem9  40640  4atlem10a  40641  4atlem10  40643  4atlem11a  40644  4atlem12a  40647  4at2  40651  2lplnm2N  40658  lneq2at  40815  2llnma1b  40823  2llnma1  40824  2llnma3r  40825  2llnma2  40826  2llnma2rN  40827  cdlema1N  40828  paddasslem2  40858  paddasslem16  40872  pmodlem1  40883  pmod2iN  40886  hlmod1i  40893  atmod2i1  40898  atmod2i2  40899  atmod3i1  40901  atmod3i2  40902  atmod4i1  40903  atmod4i2  40904  llnexchb2lem  40905  llnexch2N  40907  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem13  40920  dalawlem15  40922  osumcllem7N  40999  osumcllem9N  41001  pl42lem1N  41016  4atexlemswapqr  41100  4atex2  41114  4atex2-0bOLDN  41116  trlval4  41225  cdlemc5  41232  cdlemc6  41233  cdlemd2  41236  cdlemd4  41238  cdlemd6  41240  cdleme00a  41246  cdleme0e  41254  cdleme4  41275  cdleme4a  41276  cdleme5  41277  cdleme9  41290  cdleme16aN  41296  cdleme11c  41298  cdleme11dN  41299  cdleme11e  41300  cdleme11g  41302  cdleme11h  41303  cdleme11j  41304  cdleme11k  41305  cdleme11l  41306  cdleme11  41307  cdleme12  41308  cdleme13  41309  cdleme14  41310  cdleme15a  41311  cdleme15c  41313  cdleme16b  41316  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme17d1  41326  cdleme0nex  41327  cdleme18a  41328  cdleme18b  41329  cdleme18c  41330  cdleme18d  41332  cdlemednpq  41336  cdlemednuN  41337  cdleme20zN  41338  cdleme20y  41339  cdleme19a  41340  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20aN  41346  cdleme20d  41349  cdleme20f  41351  cdleme20g  41352  cdleme20i  41354  cdleme20j  41355  cdleme20l1  41357  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme21b  41363  cdleme21c  41364  cdleme21e  41368  cdleme21j  41373  cdleme22aa  41376  cdleme22a  41377  cdleme22b  41378  cdleme22cN  41379  cdleme22d  41380  cdleme22e  41381  cdleme22eALTN  41382  cdleme22f  41383  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme27N  41406  cdleme28a  41407  cdleme28b  41408  cdleme30a  41415  cdlemefs31fv1  41461  cdleme32b  41479  cdleme32c  41480  cdleme32e  41482  cdleme35h  41493  cdleme36a  41497  cdleme36m  41498  cdleme41sn3aw  41511  cdleme41sn4aw  41512  cdleme41fva11  41514  cdleme42k  41521  cdleme43cN  41528  cdleme46f2g1  41531  cdlemeg46fjgN  41558  cdlemeg46fjv  41560  cdlemeg46frv  41562  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemeg46gfv  41567  cdleme50trn2a  41587  cdlemg4a  41645  cdlemg4d  41650  cdlemg4e  41651  cdlemg4f  41652  cdlemg8c  41666  cdlemg9a  41669  cdlemg9b  41670  cdlemg10a  41677  cdlemg10  41678  cdlemg12b  41681  cdlemg12f  41685  cdlemg12g  41686  cdlemg12  41687  cdlemg17dN  41700  cdlemg17dALTN  41701  cdlemg17e  41702  cdlemg17f  41703  cdlemg17g  41704  cdlemg17i  41706  cdlemg17ir  41707  cdlemg17pq  41709  cdlemg17bq  41710  cdlemg17iqN  41711  cdlemg17  41714  cdlemg18b  41716  cdlemg18c  41717  cdlemg18d  41718  cdlemg18  41719  cdlemg19  41721  cdlemg21  41723  cdlemg28a  41730  cdlemg31b0a  41732  cdlemg27b  41733  cdlemg33b0  41738  cdlemg28b  41740  cdlemg28  41741  cdlemg35  41750  cdlemg36  41751  cdlemg44a  41768  cdlemh  41854  cdlemi2  41856  cdlemj1  41858  tendocan  41861  cdlemk5a  41872  cdlemk5  41873  cdlemki  41878  cdlemkvcl  41879  cdlemk10  41880  cdlemksv2  41884  cdlemk7  41885  cdlemk11  41886  cdlemk12  41887  cdlemkoatnle  41888  cdlemk15  41892  cdlemk16a  41893  cdlemk16  41894  cdlemk1u  41896  cdlemk5u  41898  cdlemk6u  41899  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk11u  41908  cdlemk12u  41909  cdlemk21N  41910  cdlemk20  41911  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk22  41930  cdlemk30  41931  cdlemkuel-3  41935  cdlemkuv2-3N  41936  cdlemk18-3N  41937  cdlemkfid1N  41958  cdlemkid1  41959  cdlemkfid3N  41962  cdlemky  41963  cdlemk11ta  41966  cdlemk47  41986  cdlemk48  41987  cdlemk49  41988  cdlemk50  41989  cdlemk51  41990  cdlemk52  41991  cdlemk53a  41992  cdlemk53  41994  cdlemk54  41995  cdlemk55a  41996  cdlemkyyN  41999  cdlemk43N  42000  cdlemk55u1  42002  cdlemk55u  42003  cdlemk39u1  42004  cdlemk19u1  42006  cdleml1N  42013  cdleml2N  42014  cdleml3N  42015  dia2dimlem6  42106  cdlemn2  42232  cdlemn2a  42233  cdlemn5pre  42237  cdlemn11a  42244  dihjustlem  42253  dihjust  42254  dihmeetlem15N  42358  lclkrlem2y  42568  aks6d1c1  43146  relexpmulnn  44694  ormkglobd  47856  iscnrm3llem1  50026  iscnrm3l  50028  swapffunc  50359  fucofunc  50436  amgmwlem  50956