Theorem simp22 1208

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 1137	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant2 1134	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp122  1307  simp222  1316  simp322  1325  elfiun  9314  cofsmo  10160  modexp  14145  funcoppc  17782  funcres  17803  catcisolem  18017  1stfcl  18103  2ndfcl  18104  prfcl  18109  evlfcl  18128  curf1cl  18134  curfcl  18138  hofcl  18165  mulgdirlem  19018  pmtrprfv3  19367  ogrpsub  20050  ogrpaddlt  20051  ogrpsublt  20055  mdetunilem4  22531  mdetuni0  22537  mdetmul  22539  prdsxmetlem  24284  isosctrlem3  26758  isosctr  26759  amgmlem  26928  f1otrg  28850  colinearalg  28889  ax5seglem6  28913  ax5seg  28917  axpasch  28920  axeuclidlem  28941  axeuclid  28942  rhmdvd  33287  bnj966  34954  mclspps  35626  cgrtr  36032  cgrtr3  36034  ofscom  36047  cgrextend  36048  btwnxfr  36096  colinearxfr  36115  lineext  36116  fscgr  36120  linecgr  36121  btwnconn1lem1  36127  btwnconn1lem2  36128  btwnconn1lem3  36129  btwnconn1lem4  36130  btwnconn1lem5  36131  btwnconn1lem6  36132  btwnconn1lem7  36133  seglecgr12im  36150  seglecgr12  36151  segletr  36154  broutsideof3  36166  outsideofeq  36170  lineunray  36187  linecom  36190  eqlkr  39144  lshpkrlem5  39159  omlmod1i2N  39305  cvrnbtwn3  39321  cvrcmp2  39329  cvlexch2  39374  cvlexchb2  39376  cvlatexchb2  39380  cvlatexch1  39381  cvlatexch2  39382  cvlatexch3  39383  cvlsupr7  39393  cvlsupr8  39394  atnlej1  39424  atnlej2  39425  2llnneN  39454  cvratlem  39466  atcvrneN  39475  atlelt  39483  2atjm  39490  3noncolr2  39494  3noncolr1N  39495  hlatcon2  39497  3dimlem2  39504  3dim1  39512  3dim2  39513  1cvrat  39521  ps-1  39522  ps-2  39523  2atjlej  39524  hlatexch3N  39525  ps-2b  39527  3atlem1  39528  3atlem5  39532  3atlem6  39533  2atm  39572  ps-2c  39573  lplni2  39582  lplnri3N  39600  llncvrlpln2  39602  2atmat  39606  2llnm2N  39613  2llnm3N  39614  2llnm4  39615  2llnmeqat  39616  lvolnle3at  39627  4atlem0ae  39639  4atlem0be  39640  4atlem3b  39643  4atlem9  39648  4atlem10a  39649  4atlem10  39651  4atlem11a  39652  4atlem12a  39655  4at2  39659  2lplnm2N  39666  lneq2at  39823  2llnma1b  39831  2llnma1  39832  2llnma3r  39833  2llnma2  39834  2llnma2rN  39835  cdlema1N  39836  paddasslem2  39866  paddasslem16  39880  pmodlem1  39891  pmod2iN  39894  hlmod1i  39901  atmod2i1  39906  atmod2i2  39907  atmod3i1  39909  atmod3i2  39910  atmod4i1  39911  atmod4i2  39912  llnexchb2lem  39913  llnexch2N  39915  dalawlem3  39918  dalawlem4  39919  dalawlem5  39920  dalawlem6  39921  dalawlem7  39922  dalawlem8  39923  dalawlem9  39924  dalawlem11  39926  dalawlem12  39927  dalawlem13  39928  dalawlem15  39930  osumcllem7N  40007  osumcllem9N  40009  pl42lem1N  40024  4atexlemswapqr  40108  4atex2  40122  4atex2-0bOLDN  40124  trlval4  40233  cdlemc5  40240  cdlemc6  40241  cdlemd2  40244  cdlemd4  40246  cdlemd6  40248  cdleme00a  40254  cdleme0e  40262  cdleme4  40283  cdleme4a  40284  cdleme5  40285  cdleme9  40298  cdleme16aN  40304  cdleme11c  40306  cdleme11dN  40307  cdleme11e  40308  cdleme11g  40310  cdleme11h  40311  cdleme11j  40312  cdleme11k  40313  cdleme11l  40314  cdleme11  40315  cdleme12  40316  cdleme13  40317  cdleme14  40318  cdleme15a  40319  cdleme15c  40321  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme16f  40328  cdleme17d1  40334  cdleme0nex  40335  cdleme18a  40336  cdleme18b  40337  cdleme18c  40338  cdleme18d  40340  cdlemednpq  40344  cdlemednuN  40345  cdleme20zN  40346  cdleme20y  40347  cdleme19a  40348  cdleme19b  40349  cdleme19d  40351  cdleme19e  40352  cdleme20aN  40354  cdleme20d  40357  cdleme20f  40359  cdleme20g  40360  cdleme20i  40362  cdleme20j  40363  cdleme20l1  40365  cdleme20l2  40366  cdleme20l  40367  cdleme20m  40368  cdleme21b  40371  cdleme21c  40372  cdleme21e  40376  cdleme21j  40381  cdleme22aa  40384  cdleme22a  40385  cdleme22b  40386  cdleme22cN  40387  cdleme22d  40388  cdleme22e  40389  cdleme22eALTN  40390  cdleme22f  40391  cdleme26fALTN  40407  cdleme26f  40408  cdleme26f2ALTN  40409  cdleme26f2  40410  cdleme27N  40414  cdleme28a  40415  cdleme28b  40416  cdleme30a  40423  cdlemefs31fv1  40469  cdleme32b  40487  cdleme32c  40488  cdleme32e  40490  cdleme35h  40501  cdleme36a  40505  cdleme36m  40506  cdleme41sn3aw  40519  cdleme41sn4aw  40520  cdleme41fva11  40522  cdleme42k  40529  cdleme43cN  40536  cdleme46f2g1  40539  cdlemeg46fjgN  40566  cdlemeg46fjv  40568  cdlemeg46frv  40570  cdlemeg46rgv  40573  cdlemeg46req  40574  cdlemeg46gfv  40575  cdleme50trn2a  40595  cdlemg4a  40653  cdlemg4d  40658  cdlemg4e  40659  cdlemg4f  40660  cdlemg8c  40674  cdlemg9a  40677  cdlemg9b  40678  cdlemg10a  40685  cdlemg10  40686  cdlemg12b  40689  cdlemg12f  40693  cdlemg12g  40694  cdlemg12  40695  cdlemg17dN  40708  cdlemg17dALTN  40709  cdlemg17e  40710  cdlemg17f  40711  cdlemg17g  40712  cdlemg17i  40714  cdlemg17ir  40715  cdlemg17pq  40717  cdlemg17bq  40718  cdlemg17iqN  40719  cdlemg17  40722  cdlemg18b  40724  cdlemg18c  40725  cdlemg18d  40726  cdlemg18  40727  cdlemg19  40729  cdlemg21  40731  cdlemg28a  40738  cdlemg31b0a  40740  cdlemg27b  40741  cdlemg33b0  40746  cdlemg28b  40748  cdlemg28  40749  cdlemg35  40758  cdlemg36  40759  cdlemg44a  40776  cdlemh  40862  cdlemi2  40864  cdlemj1  40866  tendocan  40869  cdlemk5a  40880  cdlemk5  40881  cdlemki  40886  cdlemkvcl  40887  cdlemk10  40888  cdlemksv2  40892  cdlemk7  40893  cdlemk11  40894  cdlemk12  40895  cdlemkoatnle  40896  cdlemk15  40900  cdlemk16a  40901  cdlemk16  40902  cdlemk1u  40904  cdlemk5u  40906  cdlemk6u  40907  cdlemk18  40913  cdlemk19  40914  cdlemk7u  40915  cdlemk11u  40916  cdlemk12u  40917  cdlemk21N  40918  cdlemk20  40919  cdlemkoatnle-2N  40920  cdlemk13-2N  40921  cdlemkole-2N  40922  cdlemk14-2N  40923  cdlemk15-2N  40924  cdlemk16-2N  40925  cdlemk17-2N  40926  cdlemk18-2N  40931  cdlemk19-2N  40932  cdlemk22  40938  cdlemk30  40939  cdlemkuel-3  40943  cdlemkuv2-3N  40944  cdlemk18-3N  40945  cdlemkfid1N  40966  cdlemkid1  40967  cdlemkfid3N  40970  cdlemky  40971  cdlemk11ta  40974  cdlemk47  40994  cdlemk48  40995  cdlemk49  40996  cdlemk50  40997  cdlemk51  40998  cdlemk52  40999  cdlemk53a  41000  cdlemk53  41002  cdlemk54  41003  cdlemk55a  41004  cdlemkyyN  41007  cdlemk43N  41008  cdlemk55u1  41010  cdlemk55u  41011  cdlemk39u1  41012  cdlemk19u1  41014  cdleml1N  41021  cdleml2N  41022  cdleml3N  41023  dia2dimlem6  41114  cdlemn2  41240  cdlemn2a  41241  cdlemn5pre  41245  cdlemn11a  41252  dihjustlem  41261  dihjust  41262  dihmeetlem15N  41366  lclkrlem2y  41576  aks6d1c1  42155  relexpmulnn  43748  ormkglobd  46919  natglobalincr  46921  iscnrm3llem1  48986  iscnrm3l  48988  swapffunc  49320  fucofunc  49397  amgmwlem  49840