Theorem simp31 1210

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

Assertion

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

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 1137	. 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:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7380  smogt  8407  frlmphl  21801  mdetuni0  22627  mdetmul  22629  gsummatr01lem3  22663  decpmatmullem  22777  tsmsxp  24163  log2sumbnd  27588  nosupres  27752  noinfres  27767  ax5seg  28953  wlkoniswlk  29679  iocinioc2  32781  totprob  34429  cgrtr  35993  cgrtr3  35995  ofscom  36008  cgrextend  36009  segconeq  36011  ifscgr  36045  btwnxfr  36057  colinearxfr  36076  brofs2  36078  brifs2  36079  fscgr  36081  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem12  36099  seglecgr12im  36111  seglecgr12  36112  segletr  36115  outsideofeq  36131  ivthALT  36336  lshpkrlem5  39115  lshpkrlem6  39116  exatleN  39406  atbtwn  39448  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  2atmat  39563  4atlem11b  39610  4atlem11  39611  4at  39615  4at2  39616  2lplnja  39621  2lplnj  39622  dalemswapyz  39658  dalemccnedd  39689  cdlemb  39796  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  4atex2  40079  4atex2-0bOLDN  40081  4atex3  40083  ltrn11at  40149  trlval3  40189  cdlemd3  40202  cdleme0moN  40227  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  cdleme15b  40277  cdleme15c  40278  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme17c  40290  cdleme18c  40295  cdleme18d  40297  cdlemeda  40300  cdleme19a  40305  cdleme19b  40306  cdleme19c  40307  cdleme20aN  40311  cdleme20bN  40312  cdleme20d  40314  cdleme20i  40319  cdleme20j  40320  cdleme20l1  40322  cdleme20l2  40323  cdleme21d  40332  cdleme21e  40333  cdleme21f  40334  cdleme22aa  40341  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f2  40349  cdleme22g  40350  cdleme23b  40352  cdleme26eALTN  40363  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme28a  40372  cdleme28b  40373  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35h  40458  cdleme35sn2aw  40460  cdleme41sn3aw  40476  cdleme41sn4aw  40477  cdlemeg46gfre  40534  cdlemf1  40563  cdlemg1cex  40590  cdlemg2ce  40594  cdlemg4d  40615  cdlemg4e  40616  cdlemg4f  40617  cdlemg4  40619  cdlemg6d  40623  cdlemg6e  40624  cdlemg7fvN  40626  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg9b  40635  cdlemg9  40636  cdlemg11aq  40640  cdlemg10a  40642  cdlemg12a  40645  cdlemg12b  40646  cdlemg12c  40647  cdlemg12d  40648  cdlemg13  40654  cdlemg14f  40655  cdlemg14g  40656  cdlemg17b  40664  cdlemg17dN  40665  cdlemg17e  40667  cdlemg17i  40671  cdlemg17pq  40674  cdlemg17iqN  40676  cdlemg18c  40682  cdlemg18d  40683  cdlemg18  40684  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg31b0N  40696  cdlemg27b  40698  cdlemg31c  40701  cdlemg33b0  40703  cdlemg33c0  40704  cdlemg33  40713  cdlemg35  40715  cdlemg43  40732  cdlemg44a  40733  cdlemg46  40737  cdlemh2  40818  cdlemh  40819  cdlemj1  40823  cdlemk3  40835  cdlemk5  40838  cdlemk6  40839  cdlemki  40843  cdlemksv2  40849  cdlemk12  40852  cdlemk15  40857  cdlemk16  40859  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  cdlemk20-2N  40894  cdlemk22  40895  cdlemk30  40896  cdlemk31  40898  cdlemk24-3  40905  cdlemkid2  40926  cdlemkfid3N  40927  cdlemk11ta  40931  cdlemkid3N  40935  cdlemk11tc  40947  cdlemk45  40949  cdlemk46  40950  cdlemk47  40951  cdlemk52  40956  cdlemk53a  40957  cdlemk53b  40958  cdleml1N  40978  cdleml3N  40980  cdlemn7  41205  cdlemn10  41208  dihordlem7  41216  dihord1  41220  dihord11c  41226  dihord2  41229  hlhilphllem  41965  fmuldfeq  45598  seposep  48823  iscnrm3rlem8  48844  iscnrm3llem2  48847