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

This theorem is referenced by:  simp122  1305  simp222  1314  simp322  1323  elfiun  9467  cofsmo  10306  modexp  14273  funcoppc  17925  funcres  17946  catcisolem  18163  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  mulgdirlem  19135  pmtrprfv3  19486  mdetunilem4  22636  mdetuni0  22642  mdetmul  22644  prdsxmetlem  24393  isosctrlem3  26877  isosctr  26878  amgmlem  27047  f1otrg  28893  colinearalg  28939  ax5seglem6  28963  ax5seg  28967  axpasch  28970  axeuclidlem  28991  axeuclid  28992  ogrpsub  33075  ogrpaddlt  33076  ogrpsublt  33080  rhmdvd  33327  bnj966  34936  mclspps  35568  cgrtr  35973  cgrtr3  35975  ofscom  35988  cgrextend  35989  btwnxfr  36037  colinearxfr  36056  lineext  36057  fscgr  36061  linecgr  36062  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem7  36074  seglecgr12im  36091  seglecgr12  36092  segletr  36095  broutsideof3  36107  outsideofeq  36111  lineunray  36128  linecom  36131  eqlkr  39080  lshpkrlem5  39095  omlmod1i2N  39241  cvrnbtwn3  39257  cvrcmp2  39265  cvlexch2  39310  cvlexchb2  39312  cvlatexchb2  39316  cvlatexch1  39317  cvlatexch2  39318  cvlatexch3  39319  cvlsupr7  39329  cvlsupr8  39330  atnlej1  39361  atnlej2  39362  2llnneN  39391  cvratlem  39403  atcvrneN  39412  atlelt  39420  2atjm  39427  3noncolr2  39431  3noncolr1N  39432  hlatcon2  39434  3dimlem2  39441  3dim1  39449  3dim2  39450  1cvrat  39458  ps-1  39459  ps-2  39460  2atjlej  39461  hlatexch3N  39462  ps-2b  39464  3atlem1  39465  3atlem5  39469  3atlem6  39470  2atm  39509  ps-2c  39510  lplni2  39519  lplnri3N  39537  llncvrlpln2  39539  2atmat  39543  2llnm2N  39550  2llnm3N  39551  2llnm4  39552  2llnmeqat  39553  lvolnle3at  39564  4atlem0ae  39576  4atlem0be  39577  4atlem3b  39580  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem12a  39592  4at2  39596  2lplnm2N  39603  lneq2at  39760  2llnma1b  39768  2llnma1  39769  2llnma3r  39770  2llnma2  39771  2llnma2rN  39772  cdlema1N  39773  paddasslem2  39803  paddasslem16  39817  pmodlem1  39828  pmod2iN  39831  hlmod1i  39838  atmod2i1  39843  atmod2i2  39844  atmod3i1  39846  atmod3i2  39847  atmod4i1  39848  atmod4i2  39849  llnexchb2lem  39850  llnexch2N  39852  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem13  39865  dalawlem15  39867  osumcllem7N  39944  osumcllem9N  39946  pl42lem1N  39961  4atexlemswapqr  40045  4atex2  40059  4atex2-0bOLDN  40061  trlval4  40170  cdlemc5  40177  cdlemc6  40178  cdlemd2  40181  cdlemd4  40183  cdlemd6  40185  cdleme00a  40191  cdleme0e  40199  cdleme4  40220  cdleme4a  40221  cdleme5  40222  cdleme9  40235  cdleme16aN  40241  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11g  40247  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme11l  40251  cdleme11  40252  cdleme12  40253  cdleme13  40254  cdleme14  40255  cdleme15a  40256  cdleme15c  40258  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme17d1  40271  cdleme0nex  40272  cdleme18a  40273  cdleme18b  40274  cdleme18c  40275  cdleme18d  40277  cdlemednpq  40281  cdlemednuN  40282  cdleme20zN  40283  cdleme20y  40284  cdleme19a  40285  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20aN  40291  cdleme20d  40294  cdleme20f  40296  cdleme20g  40297  cdleme20i  40299  cdleme20j  40300  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21b  40308  cdleme21c  40309  cdleme21e  40313  cdleme21j  40318  cdleme22aa  40321  cdleme22a  40322  cdleme22b  40323  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme30a  40360  cdlemefs31fv1  40406  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35h  40438  cdleme36a  40442  cdleme36m  40443  cdleme41sn3aw  40456  cdleme41sn4aw  40457  cdleme41fva11  40459  cdleme42k  40466  cdleme43cN  40473  cdleme46f2g1  40476  cdlemeg46fjgN  40503  cdlemeg46fjv  40505  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme50trn2a  40532  cdlemg4a  40590  cdlemg4d  40595  cdlemg4e  40596  cdlemg4f  40597  cdlemg8c  40611  cdlemg9a  40614  cdlemg9b  40615  cdlemg10a  40622  cdlemg10  40623  cdlemg12b  40626  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg17dN  40645  cdlemg17dALTN  40646  cdlemg17e  40647  cdlemg17f  40648  cdlemg17g  40649  cdlemg17i  40651  cdlemg17ir  40652  cdlemg17pq  40654  cdlemg17bq  40655  cdlemg17iqN  40656  cdlemg17  40659  cdlemg18b  40661  cdlemg18c  40662  cdlemg18d  40663  cdlemg18  40664  cdlemg19  40666  cdlemg21  40668  cdlemg28a  40675  cdlemg31b0a  40677  cdlemg27b  40678  cdlemg33b0  40683  cdlemg28b  40685  cdlemg28  40686  cdlemg35  40695  cdlemg36  40696  cdlemg44a  40713  cdlemh  40799  cdlemi2  40801  cdlemj1  40803  tendocan  40806  cdlemk5a  40817  cdlemk5  40818  cdlemki  40823  cdlemkvcl  40824  cdlemk10  40825  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemkoatnle  40833  cdlemk15  40837  cdlemk16a  40838  cdlemk16  40839  cdlemk1u  40841  cdlemk5u  40843  cdlemk6u  40844  cdlemk18  40850  cdlemk19  40851  cdlemk7u  40852  cdlemk11u  40853  cdlemk12u  40854  cdlemk21N  40855  cdlemk20  40856  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk22  40875  cdlemk30  40876  cdlemkuel-3  40880  cdlemkuv2-3N  40881  cdlemk18-3N  40882  cdlemkfid1N  40903  cdlemkid1  40904  cdlemkfid3N  40907  cdlemky  40908  cdlemk11ta  40911  cdlemk47  40931  cdlemk48  40932  cdlemk49  40933  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdlemk53  40939  cdlemk54  40940  cdlemk55a  40941  cdlemkyyN  40944  cdlemk43N  40945  cdlemk55u1  40947  cdlemk55u  40948  cdlemk39u1  40949  cdlemk19u1  40951  cdleml1N  40958  cdleml2N  40959  cdleml3N  40960  dia2dimlem6  41051  cdlemn2  41177  cdlemn2a  41178  cdlemn5pre  41182  cdlemn11a  41189  dihjustlem  41198  dihjust  41199  dihmeetlem15N  41303  lclkrlem2y  41513  aks6d1c1  42097  relexpmulnn  43698  natglobalincr  46830  iscnrm3llem1  48745  iscnrm3l  48747  amgmwlem  49032