Theorem simp32 1211

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp32	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1136	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp132  1310  simp232  1319  simp332  1328  eqfunresadj  7380  smogt  8407  axdc3lem4  10493  bitsfzo  16472  frlmphl  21801  mdetunilem4  22621  mdetuni0  22627  mdetmul  22629  decpmatmullem  22777  logfacbnd3  27267  logexprlim  27269  log2sumbnd  27588  nosupfv  27751  nosupres  27752  noinffv  27766  noinfres  27767  ax5seg  28953  numclwwlk1lem2foa  30373  iocinioc2  32781  totprob  34429  cgrtr  35993  cgrtr3  35995  ofscom  36008  cgrextend  36009  segconeq  36011  ifscgr  36045  colinearxfr  36076  brofs2  36078  brifs2  36079  fscgr  36081  btwnconn1lem2  36089  btwnconn1lem9  36096  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem12  36099  brsegle2  36110  seglecgr12im  36111  seglecgr12  36112  segletr  36115  outsideofeq  36131  ivthALT  36336  lshpkrlem5  39115  lshpkrlem6  39116  atbtwnexOLDN  39449  atbtwnex  39450  4noncolr3  39455  3dimlem3a  39462  3dim1  39469  3dim2  39470  1cvrat  39478  2atjlej  39481  hlatexch4  39483  ps-2b  39484  2atm  39529  ps-2c  39530  2atmat  39563  4atlem10  39608  4atlem11b  39610  4atlem11  39611  4at  39615  4at2  39616  2lplnja  39621  2lplnj  39622  dalemswapyz  39658  dalem-ddly  39688  cdlemb  39796  paddasslem5  39826  pmodlem1  39848  dalawlem1  39873  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem15  39887  osumcllem5N  39962  osumcllem6N  39963  lhpexle3lem  40013  lhpmcvr4N  40028  lhpmcvr6N  40030  4atexlemex6  40076  4atex2  40079  4atex2-0bOLDN  40081  4atex2-0cOLDN  40082  ltrn11at  40149  trlval3  40189  cdlemd3  40202  cdleme7aa  40244  cdleme7b  40246  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme16aN  40261  cdleme11dN  40264  cdleme11e  40265  cdleme11l  40271  cdleme11  40272  cdleme12  40273  cdleme14  40275  cdleme15a  40276  cdleme15c  40278  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme17c  40290  cdleme18c  40295  cdlemeda  40300  cdlemednpq  40301  cdleme19a  40305  cdleme19c  40307  cdleme20aN  40311  cdleme20bN  40312  cdleme20l1  40322  cdleme20l2  40323  cdleme22aa  40341  cdleme22a  40342  cdleme22g  40350  cdleme23b  40352  cdleme23c  40353  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme28b  40373  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35h  40458  cdleme35sn2aw  40460  cdleme38m  40465  cdleme40n  40470  cdleme41sn3aw  40476  cdleme41sn4aw  40477  cdlemeg46gfre  40534  cdlemf1  40563  cdlemg1cex  40590  cdlemg2ce  40594  cdlemg4d  40615  cdlemg4  40619  cdlemg7fvN  40626  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg11aq  40640  cdlemg10a  40642  cdlemg12a  40645  cdlemg12b  40646  cdlemg12d  40648  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg13  40654  cdlemg14f  40655  cdlemg14g  40656  cdlemg17b  40664  cdlemg17dN  40665  cdlemg17e  40667  cdlemg17pq  40674  cdlemg17iqN  40676  cdlemg18c  40682  cdlemg18d  40683  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg28a  40695  cdlemg31b0N  40696  cdlemg27b  40698  cdlemg31c  40701  cdlemg33b0  40703  cdlemg28  40706  cdlemg33a  40708  cdlemg33  40713  cdlemg35  40715  cdlemg36  40716  cdlemg44a  40733  cdlemg46  40737  cdlemh2  40818  cdlemh  40819  cdlemj1  40823  cdlemk5  40838  cdlemk6  40839  cdlemki  40843  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemkole  40855  cdlemk14  40856  cdlemk16  40859  cdlemk1u  40861  cdlemk18  40870  cdlemk19  40871  cdlemk7u  40872  cdlemk11u  40873  cdlemk33N  40911  cdlemkid2  40926  cdlemkfid3N  40927  cdlemk11ta  40931  cdlemk11tc  40947  cdlemk45  40949  cdlemk46  40950  cdlemk47  40951  cdlemk52  40956  cdlemk53a  40957  cdlemk54  40960  cdlemk55a  40961  cdleml1N  40978  cdleml3N  40980  cdlemn7  41205  cdlemn8  41206  cdlemn10  41208  dihordlem7  41216  dihordlem7b  41217  dihord1  41220  dihord10  41225  dihord11c  41226  dihord2  41229  hlhilphllem  41965  fmuldfeq  45598  seposep  48823  iscnrm3rlem8  48844  iscnrm3llem2  48847