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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7357  smogt  8367  frlmphl  21336  mdetuni0  22123  mdetmul  22125  gsummatr01lem3  22159  decpmatmullem  22273  tsmsxp  23659  log2sumbnd  27047  nosupres  27210  noinfres  27225  ax5seg  28196  wlkoniswlk  28918  iocinioc2  31990  totprob  33426  cgrtr  34964  cgrtr3  34966  ofscom  34979  cgrextend  34980  segconeq  34982  ifscgr  35016  btwnxfr  35028  colinearxfr  35047  brofs2  35049  brifs2  35050  fscgr  35052  btwnconn1lem1  35059  btwnconn1lem2  35060  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem7  35065  btwnconn1lem8  35066  btwnconn1lem9  35067  btwnconn1lem10  35068  btwnconn1lem11  35069  btwnconn1lem12  35070  seglecgr12im  35082  seglecgr12  35083  segletr  35086  outsideofeq  35102  ivthALT  35220  lshpkrlem5  37984  lshpkrlem6  37985  exatleN  38275  atbtwn  38317  atbtwnexOLDN  38318  atbtwnex  38319  4noncolr3  38324  3dimlem3a  38331  3dimlem4a  38334  3dim1  38338  3dim2  38339  1cvrat  38347  2atjlej  38350  hlatexch4  38352  ps-2b  38353  2atm  38398  2atmat  38432  4atlem11b  38479  4atlem11  38480  4at  38484  4at2  38485  2lplnja  38490  2lplnj  38491  dalemswapyz  38527  dalemccnedd  38558  cdlemb  38665  paddasslem5  38695  paddasslem15  38705  pmodlem1  38717  dalawlem1  38742  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem12  38753  dalawlem15  38756  osumcllem5N  38831  osumcllem6N  38832  lhpexle3lem  38882  lhpmcvr4N  38897  lhpmcvr6N  38899  4atex2  38948  4atex2-0bOLDN  38950  4atex3  38952  ltrn11at  39018  trlval3  39058  cdlemd3  39071  cdleme0moN  39096  cdleme7aa  39113  cdleme7b  39115  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme16aN  39130  cdleme11dN  39133  cdleme11e  39134  cdleme11l  39140  cdleme11  39141  cdleme12  39142  cdleme14  39144  cdleme15b  39146  cdleme15c  39147  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme16e  39153  cdleme16f  39154  cdleme17c  39159  cdleme18c  39164  cdleme18d  39166  cdlemeda  39169  cdleme19a  39174  cdleme19b  39175  cdleme19c  39176  cdleme20aN  39180  cdleme20bN  39181  cdleme20d  39183  cdleme20i  39188  cdleme20j  39189  cdleme20l1  39191  cdleme20l2  39192  cdleme21d  39201  cdleme21e  39202  cdleme21f  39203  cdleme22aa  39210  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f2  39218  cdleme22g  39219  cdleme23b  39221  cdleme26eALTN  39232  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme28a  39241  cdleme28b  39242  cdleme32b  39313  cdleme32c  39314  cdleme32e  39316  cdleme35h  39327  cdleme35sn2aw  39329  cdleme41sn3aw  39345  cdleme41sn4aw  39346  cdlemeg46gfre  39403  cdlemf1  39432  cdlemg1cex  39459  cdlemg2ce  39463  cdlemg4d  39484  cdlemg4e  39485  cdlemg4f  39486  cdlemg4  39488  cdlemg6d  39492  cdlemg6e  39493  cdlemg7fvN  39495  cdlemg8b  39499  cdlemg8c  39500  cdlemg9a  39503  cdlemg9b  39504  cdlemg9  39505  cdlemg11aq  39509  cdlemg10a  39511  cdlemg12a  39514  cdlemg12b  39515  cdlemg12c  39516  cdlemg12d  39517  cdlemg13  39523  cdlemg14f  39524  cdlemg14g  39525  cdlemg17b  39533  cdlemg17dN  39534  cdlemg17e  39536  cdlemg17i  39540  cdlemg17pq  39543  cdlemg17iqN  39545  cdlemg18c  39551  cdlemg18d  39552  cdlemg18  39553  cdlemg19  39555  cdlemg21  39557  cdlemg27a  39563  cdlemg31b0N  39565  cdlemg27b  39567  cdlemg31c  39570  cdlemg33b0  39572  cdlemg33c0  39573  cdlemg33  39582  cdlemg35  39584  cdlemg43  39601  cdlemg44a  39602  cdlemg46  39606  cdlemh2  39687  cdlemh  39688  cdlemj1  39692  cdlemk3  39704  cdlemk5  39707  cdlemk6  39708  cdlemki  39712  cdlemksv2  39718  cdlemk12  39721  cdlemk15  39726  cdlemk16  39728  cdlemk18  39739  cdlemk19  39740  cdlemk7u  39741  cdlemk12u  39743  cdlemkoatnle-2N  39746  cdlemk13-2N  39747  cdlemkole-2N  39748  cdlemk14-2N  39749  cdlemk15-2N  39750  cdlemk16-2N  39751  cdlemk17-2N  39752  cdlemk18-2N  39757  cdlemk19-2N  39758  cdlemk7u-2N  39759  cdlemk11u-2N  39760  cdlemk12u-2N  39761  cdlemk20-2N  39763  cdlemk22  39764  cdlemk30  39765  cdlemk31  39767  cdlemk24-3  39774  cdlemkid2  39795  cdlemkfid3N  39796  cdlemk11ta  39800  cdlemkid3N  39804  cdlemk11tc  39816  cdlemk45  39818  cdlemk46  39819  cdlemk47  39820  cdlemk52  39825  cdlemk53a  39826  cdlemk53b  39827  cdleml1N  39847  cdleml3N  39849  cdlemn7  40074  cdlemn10  40077  dihordlem7  40085  dihord1  40089  dihord11c  40095  dihord2  40098  hlhilphllem  40834  fmuldfeq  44299  seposep  47558  iscnrm3rlem8  47580  iscnrm3llem2  47583