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  9339  cofsmo  10182  modexp  14163  funcoppc  17800  funcres  17821  catcisolem  18035  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  mulgdirlem  19002  pmtrprfv3  19351  ogrpsub  20034  ogrpaddlt  20035  ogrpsublt  20039  mdetunilem4  22518  mdetuni0  22524  mdetmul  22526  prdsxmetlem  24272  isosctrlem3  26746  isosctr  26747  amgmlem  26916  f1otrg  28834  colinearalg  28873  ax5seglem6  28897  ax5seg  28901  axpasch  28904  axeuclidlem  28925  axeuclid  28926  rhmdvd  33275  bnj966  34913  mclspps  35559  cgrtr  35968  cgrtr3  35970  ofscom  35983  cgrextend  35984  btwnxfr  36032  colinearxfr  36051  lineext  36052  fscgr  36056  linecgr  36057  btwnconn1lem1  36063  btwnconn1lem2  36064  btwnconn1lem3  36065  btwnconn1lem4  36066  btwnconn1lem5  36067  btwnconn1lem6  36068  btwnconn1lem7  36069  seglecgr12im  36086  seglecgr12  36087  segletr  36090  broutsideof3  36102  outsideofeq  36106  lineunray  36123  linecom  36126  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  42092  relexpmulnn  43685  ormkglobd  46860  natglobalincr  46862  iscnrm3llem1  48937  iscnrm3l  48939  swapffunc  49271  fucofunc  49348  amgmwlem  49791