Theorem simp31 1228

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 1154	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp131  1327  simp231  1336  simp331  1345  eqfunresadj  7368  smogt  8368  frlmphl  22080  mdetuni0  22929  mdetmul  22931  gsummatr01lem3  22965  decpmatmullem  23082  tsmsxp  24467  log2sumbnd  27864  nosupres  28057  noinfres  28072  ax5seg  29509  wlkoniswlk  30233  iocinioc2  33364  totprob  35052  cgrtr  36737  cgrtr3  36739  ofscom  36752  cgrextend  36753  segconeq  36755  ifscgr  36789  btwnxfr  36801  colinearxfr  36820  brofs2  36822  brifs2  36823  fscgr  36825  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem7  36838  btwnconn1lem8  36839  btwnconn1lem9  36840  btwnconn1lem10  36841  btwnconn1lem11  36842  btwnconn1lem12  36843  seglecgr12im  36855  seglecgr12  36856  segletr  36859  outsideofeq  36875  ivthALT  37103  lshpkrlem5  40151  lshpkrlem6  40152  exatleN  40441  atbtwn  40483  atbtwnexOLDN  40484  atbtwnex  40485  4noncolr3  40490  3dimlem3a  40497  3dimlem4a  40500  3dim1  40504  3dim2  40505  1cvrat  40513  2atjlej  40516  hlatexch4  40518  ps-2b  40519  2atm  40564  2atmat  40598  4atlem11b  40645  4atlem11  40646  4at  40650  4at2  40651  2lplnja  40656  2lplnj  40657  dalemswapyz  40693  dalemccnedd  40724  cdlemb  40831  paddasslem5  40861  paddasslem15  40871  pmodlem1  40883  dalawlem1  40908  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem15  40922  osumcllem5N  40997  osumcllem6N  40998  lhpexle3lem  41048  lhpmcvr4N  41063  lhpmcvr6N  41065  4atex2  41114  4atex2-0bOLDN  41116  4atex3  41118  ltrn11at  41184  trlval3  41224  cdlemd3  41237  cdleme0moN  41262  cdleme7aa  41279  cdleme7b  41281  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme7ga  41285  cdleme7  41286  cdleme16aN  41296  cdleme11dN  41299  cdleme11e  41300  cdleme11l  41306  cdleme11  41307  cdleme12  41308  cdleme14  41310  cdleme15b  41312  cdleme15c  41313  cdleme16b  41316  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme17c  41325  cdleme18c  41330  cdleme18d  41332  cdlemeda  41335  cdleme19a  41340  cdleme19b  41341  cdleme19c  41342  cdleme20aN  41346  cdleme20bN  41347  cdleme20d  41349  cdleme20i  41354  cdleme20j  41355  cdleme20l1  41357  cdleme20l2  41358  cdleme21d  41367  cdleme21e  41368  cdleme21f  41369  cdleme22aa  41376  cdleme22e  41381  cdleme22eALTN  41382  cdleme22f2  41384  cdleme22g  41385  cdleme23b  41387  cdleme26eALTN  41398  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme28a  41407  cdleme28b  41408  cdleme32b  41479  cdleme32c  41480  cdleme32e  41482  cdleme35h  41493  cdleme35sn2aw  41495  cdleme41sn3aw  41511  cdleme41sn4aw  41512  cdlemeg46gfre  41569  cdlemf1  41598  cdlemg1cex  41625  cdlemg2ce  41629  cdlemg4d  41650  cdlemg4e  41651  cdlemg4f  41652  cdlemg4  41654  cdlemg6d  41658  cdlemg6e  41659  cdlemg7fvN  41661  cdlemg8b  41665  cdlemg8c  41666  cdlemg9a  41669  cdlemg9b  41670  cdlemg9  41671  cdlemg11aq  41675  cdlemg10a  41677  cdlemg12a  41680  cdlemg12b  41681  cdlemg12c  41682  cdlemg12d  41683  cdlemg13  41689  cdlemg14f  41690  cdlemg14g  41691  cdlemg17b  41699  cdlemg17dN  41700  cdlemg17e  41702  cdlemg17i  41706  cdlemg17pq  41709  cdlemg17iqN  41711  cdlemg18c  41717  cdlemg18d  41718  cdlemg18  41719  cdlemg19  41721  cdlemg21  41723  cdlemg27a  41729  cdlemg31b0N  41731  cdlemg27b  41733  cdlemg31c  41736  cdlemg33b0  41738  cdlemg33c0  41739  cdlemg33  41748  cdlemg35  41750  cdlemg43  41767  cdlemg44a  41768  cdlemg46  41772  cdlemh2  41853  cdlemh  41854  cdlemj1  41858  cdlemk3  41870  cdlemk5  41873  cdlemk6  41874  cdlemki  41878  cdlemksv2  41884  cdlemk12  41887  cdlemk15  41892  cdlemk16  41894  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk12u  41909  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk7u-2N  41925  cdlemk11u-2N  41926  cdlemk12u-2N  41927  cdlemk20-2N  41929  cdlemk22  41930  cdlemk30  41931  cdlemk31  41933  cdlemk24-3  41940  cdlemkid2  41961  cdlemkfid3N  41962  cdlemk11ta  41966  cdlemkid3N  41970  cdlemk11tc  41982  cdlemk45  41984  cdlemk46  41985  cdlemk47  41986  cdlemk52  41991  cdlemk53a  41992  cdlemk53b  41993  cdleml1N  42013  cdleml3N  42015  cdlemn7  42240  cdlemn10  42243  dihordlem7  42251  dihord1  42255  dihord11c  42261  dihord2  42264  hlhilphllem  42996  fmuldfeq  46564  seposep  50003  iscnrm3rlem8  50024  iscnrm3llem2  50027