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  9388  cofsmo  10229  modexp  14210  funcoppc  17844  funcres  17865  catcisolem  18079  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  mulgdirlem  19044  pmtrprfv3  19391  mdetunilem4  22509  mdetuni0  22515  mdetmul  22517  prdsxmetlem  24263  isosctrlem3  26737  isosctr  26738  amgmlem  26907  f1otrg  28805  colinearalg  28844  ax5seglem6  28868  ax5seg  28872  axpasch  28875  axeuclidlem  28896  axeuclid  28897  ogrpsub  33037  ogrpaddlt  33038  ogrpsublt  33042  rhmdvd  33303  bnj966  34941  mclspps  35578  cgrtr  35987  cgrtr3  35989  ofscom  36002  cgrextend  36003  btwnxfr  36051  colinearxfr  36070  lineext  36071  fscgr  36075  linecgr  36076  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  seglecgr12im  36105  seglecgr12  36106  segletr  36109  broutsideof3  36121  outsideofeq  36125  lineunray  36142  linecom  36145  eqlkr  39099  lshpkrlem5  39114  omlmod1i2N  39260  cvrnbtwn3  39276  cvrcmp2  39284  cvlexch2  39329  cvlexchb2  39331  cvlatexchb2  39335  cvlatexch1  39336  cvlatexch2  39337  cvlatexch3  39338  cvlsupr7  39348  cvlsupr8  39349  atnlej1  39380  atnlej2  39381  2llnneN  39410  cvratlem  39422  atcvrneN  39431  atlelt  39439  2atjm  39446  3noncolr2  39450  3noncolr1N  39451  hlatcon2  39453  3dimlem2  39460  3dim1  39468  3dim2  39469  1cvrat  39477  ps-1  39478  ps-2  39479  2atjlej  39480  hlatexch3N  39481  ps-2b  39483  3atlem1  39484  3atlem5  39488  3atlem6  39489  2atm  39528  ps-2c  39529  lplni2  39538  lplnri3N  39556  llncvrlpln2  39558  2atmat  39562  2llnm2N  39569  2llnm3N  39570  2llnm4  39571  2llnmeqat  39572  lvolnle3at  39583  4atlem0ae  39595  4atlem0be  39596  4atlem3b  39599  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem12a  39611  4at2  39615  2lplnm2N  39622  lneq2at  39779  2llnma1b  39787  2llnma1  39788  2llnma3r  39789  2llnma2  39790  2llnma2rN  39791  cdlema1N  39792  paddasslem2  39822  paddasslem16  39836  pmodlem1  39847  pmod2iN  39850  hlmod1i  39857  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  atmod3i2  39866  atmod4i1  39867  atmod4i2  39868  llnexchb2lem  39869  llnexch2N  39871  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem13  39884  dalawlem15  39886  osumcllem7N  39963  osumcllem9N  39965  pl42lem1N  39980  4atexlemswapqr  40064  4atex2  40078  4atex2-0bOLDN  40080  trlval4  40189  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdlemd4  40202  cdlemd6  40204  cdleme00a  40210  cdleme0e  40218  cdleme4  40239  cdleme4a  40240  cdleme5  40241  cdleme9  40254  cdleme16aN  40260  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11g  40266  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme11l  40270  cdleme11  40271  cdleme12  40272  cdleme13  40273  cdleme14  40274  cdleme15a  40275  cdleme15c  40277  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme17d1  40290  cdleme0nex  40291  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme18d  40296  cdlemednpq  40300  cdlemednuN  40301  cdleme20zN  40302  cdleme20y  40303  cdleme19a  40304  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20aN  40310  cdleme20d  40313  cdleme20f  40315  cdleme20g  40316  cdleme20i  40318  cdleme20j  40319  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21b  40327  cdleme21c  40328  cdleme21e  40332  cdleme21j  40337  cdleme22aa  40340  cdleme22a  40341  cdleme22b  40342  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme30a  40379  cdlemefs31fv1  40425  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35h  40457  cdleme36a  40461  cdleme36m  40462  cdleme41sn3aw  40475  cdleme41sn4aw  40476  cdleme41fva11  40478  cdleme42k  40485  cdleme43cN  40492  cdleme46f2g1  40495  cdlemeg46fjgN  40522  cdlemeg46fjv  40524  cdlemeg46frv  40526  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdleme50trn2a  40551  cdlemg4a  40609  cdlemg4d  40614  cdlemg4e  40615  cdlemg4f  40616  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg10a  40641  cdlemg10  40642  cdlemg12b  40645  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg17dN  40664  cdlemg17dALTN  40665  cdlemg17e  40666  cdlemg17f  40667  cdlemg17g  40668  cdlemg17i  40670  cdlemg17ir  40671  cdlemg17pq  40673  cdlemg17bq  40674  cdlemg17iqN  40675  cdlemg17  40678  cdlemg18b  40680  cdlemg18c  40681  cdlemg18d  40682  cdlemg18  40683  cdlemg19  40685  cdlemg21  40687  cdlemg28a  40694  cdlemg31b0a  40696  cdlemg27b  40697  cdlemg33b0  40702  cdlemg28b  40704  cdlemg28  40705  cdlemg35  40714  cdlemg36  40715  cdlemg44a  40732  cdlemh  40818  cdlemi2  40820  cdlemj1  40822  tendocan  40825  cdlemk5a  40836  cdlemk5  40837  cdlemki  40842  cdlemkvcl  40843  cdlemk10  40844  cdlemksv2  40848  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemkoatnle  40852  cdlemk15  40856  cdlemk16a  40857  cdlemk16  40858  cdlemk1u  40860  cdlemk5u  40862  cdlemk6u  40863  cdlemk18  40869  cdlemk19  40870  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk21N  40874  cdlemk20  40875  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk22  40894  cdlemk30  40895  cdlemkuel-3  40899  cdlemkuv2-3N  40900  cdlemk18-3N  40901  cdlemkfid1N  40922  cdlemkid1  40923  cdlemkfid3N  40926  cdlemky  40927  cdlemk11ta  40930  cdlemk47  40950  cdlemk48  40951  cdlemk49  40952  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk53a  40956  cdlemk53  40958  cdlemk54  40959  cdlemk55a  40960  cdlemkyyN  40963  cdlemk43N  40964  cdlemk55u1  40966  cdlemk55u  40967  cdlemk39u1  40968  cdlemk19u1  40970  cdleml1N  40977  cdleml2N  40978  cdleml3N  40979  dia2dimlem6  41070  cdlemn2  41196  cdlemn2a  41197  cdlemn5pre  41201  cdlemn11a  41208  dihjustlem  41217  dihjust  41218  dihmeetlem15N  41322  lclkrlem2y  41532  aks6d1c1  42111  relexpmulnn  43705  ormkglobd  46880  natglobalincr  46882  iscnrm3llem1  48941  iscnrm3l  48943  swapffunc  49275  fucofunc  49352  amgmwlem  49795