Theorem simp33 1212

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

Assertion

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

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1139	. 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:  simp133  1311  simp233  1320  simp333  1329  eqfunresadj  7380  smogt  8407  bitsfzo  16472  frlmphl  21801  mdetunilem4  22621  mdetuni0  22627  mdetmul  22629  decpmatmullem  22777  logexprlim  27269  noinfres  27767  ax5seg  28953  iocinioc2  32781  bnj966  34958  cgrtr  35993  cgrtr3  35995  ofscom  36008  segconeq  36011  btwnxfr  36057  colinearxfr  36076  fscgr  36081  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem12  36099  brsegle2  36110  seglecgr12im  36111  seglecgr12  36112  segletr  36115  outsideofeq  36131  lshpkrlem5  39115  lshpkrlem6  39116  atbtwnexOLDN  39449  atbtwnex  39450  4noncolr3  39455  3dimlem3a  39462  3dimlem4a  39465  3dim1  39469  3dim2  39470  1cvrat  39478  2atjlej  39481  hlatexch4  39483  ps-2b  39484  2atm  39529  ps-2c  39530  lvolex3N  39540  2atmat  39563  lvolnlelpln  39587  4atlem10  39608  4atlem11b  39610  4atlem11  39611  4at  39615  4at2  39616  2lplnja  39621  2lplnj  39622  dalemclccjdd  39690  paddasslem5  39826  paddasslem15  39836  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  4atex3  40083  ltrn11at  40149  cdlemd3  40202  cdleme7aa  40244  cdleme7b  40246  cdleme7c  40247  cdleme7d  40248  cdleme7ga  40250  cdleme16aN  40261  cdleme11dN  40264  cdleme11e  40265  cdleme11l  40271  cdleme11  40272  cdleme12  40273  cdleme14  40275  cdleme15c  40278  cdleme16b  40281  cdleme16d  40283  cdleme17b  40289  cdleme17c  40290  cdleme18c  40295  cdleme18d  40297  cdlemeda  40300  cdlemednpq  40301  cdleme19a  40305  cdleme19c  40307  cdleme20aN  40311  cdleme20bN  40312  cdleme20d  40314  cdleme20f  40316  cdleme20g  40317  cdleme20j  40320  cdleme20l1  40322  cdleme21f  40334  cdleme22aa  40341  cdleme22a  40342  cdleme22cN  40344  cdleme22e  40346  cdleme22f2  40349  cdleme22g  40350  cdleme23b  40352  cdleme23c  40353  cdleme26e  40361  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme28a  40372  cdleme28b  40373  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35h2  40459  cdleme38m  40465  cdleme41sn4aw  40477  cdlemf1  40563  cdlemg1cex  40590  cdlemg2ce  40594  cdlemg4d  40615  cdlemg4f  40617  cdlemg7fvN  40626  cdlemg8a  40629  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg11a  40639  cdlemg11aq  40640  cdlemg10a  40642  cdlemg11b  40644  cdlemg12a  40645  cdlemg12b  40646  cdlemg12d  40648  cdlemg12e  40649  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg13  40654  cdlemg14f  40655  cdlemg14g  40656  cdlemg17b  40664  cdlemg17dN  40665  cdlemg17e  40667  cdlemg17h  40670  cdlemg17pq  40674  cdlemg17iqN  40676  cdlemg18b  40681  cdlemg18c  40682  cdlemg18d  40683  cdlemg18  40684  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg31b0N  40696  cdlemg27b  40698  cdlemg33b0  40703  cdlemg33c0  40704  cdlemg28  40706  cdlemg33a  40708  cdlemg35  40715  cdlemg42  40731  cdlemg44a  40733  cdlemg47  40738  cdlemh2  40818  cdlemh  40819  cdlemj1  40823  cdlemk3  40835  cdlemk5  40838  cdlemki  40843  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk16a  40858  cdlemk16  40859  cdlemkj  40865  cdlemkuv2  40869  cdlemk18  40870  cdlemk19  40871  cdlemk7u  40872  cdlemk12u  40874  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk21-2N  40893  cdlemk20-2N  40894  cdlemk22  40895  cdlemk30  40896  cdlemk31  40898  cdlemk32  40899  cdlemk24-3  40905  cdlemkid2  40926  cdlemkfid3N  40927  cdlemk45  40949  cdlemk46  40950  cdlemk47  40951  cdlemk52  40956  cdlemk53a  40957  cdleml1N  40978  cdleml3N  40980  cdlemn7  41205  cdlemn10  41208  dihordlem7  41216  dihord1  41220  dihord2a  41221  dihord10  41225  dihord11c  41226  dihord2pre2  41228  hlhilphllem  41965  fmuldfeq  45598  usgrgrtrirex  47917  seposep  48823  iscnrm3rlem8  48844  iscnrm3llem2  48847