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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7335  smogt  8336  frlmphl  21690  mdetuni0  22508  mdetmul  22510  gsummatr01lem3  22544  decpmatmullem  22658  tsmsxp  24042  log2sumbnd  27455  nosupres  27619  noinfres  27634  ax5seg  28865  wlkoniswlk  29589  iocinioc2  32702  totprob  34418  cgrtr  35980  cgrtr3  35982  ofscom  35995  cgrextend  35996  segconeq  35998  ifscgr  36032  btwnxfr  36044  colinearxfr  36063  brofs2  36065  brifs2  36066  fscgr  36068  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem10  36084  btwnconn1lem11  36085  btwnconn1lem12  36086  seglecgr12im  36098  seglecgr12  36099  segletr  36102  outsideofeq  36118  ivthALT  36323  lshpkrlem5  39107  lshpkrlem6  39108  exatleN  39398  atbtwn  39440  atbtwnexOLDN  39441  atbtwnex  39442  4noncolr3  39447  3dimlem3a  39454  3dimlem4a  39457  3dim1  39461  3dim2  39462  1cvrat  39470  2atjlej  39473  hlatexch4  39475  ps-2b  39476  2atm  39521  2atmat  39555  4atlem11b  39602  4atlem11  39603  4at  39607  4at2  39608  2lplnja  39613  2lplnj  39614  dalemswapyz  39650  dalemccnedd  39681  cdlemb  39788  paddasslem5  39818  paddasslem15  39828  pmodlem1  39840  dalawlem1  39865  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem15  39879  osumcllem5N  39954  osumcllem6N  39955  lhpexle3lem  40005  lhpmcvr4N  40020  lhpmcvr6N  40022  4atex2  40071  4atex2-0bOLDN  40073  4atex3  40075  ltrn11at  40141  trlval3  40181  cdlemd3  40194  cdleme0moN  40219  cdleme7aa  40236  cdleme7b  40238  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme16aN  40253  cdleme11dN  40256  cdleme11e  40257  cdleme11l  40263  cdleme11  40264  cdleme12  40265  cdleme14  40267  cdleme15b  40269  cdleme15c  40270  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme17c  40282  cdleme18c  40287  cdleme18d  40289  cdlemeda  40292  cdleme19a  40297  cdleme19b  40298  cdleme19c  40299  cdleme20aN  40303  cdleme20bN  40304  cdleme20d  40306  cdleme20i  40311  cdleme20j  40312  cdleme20l1  40314  cdleme20l2  40315  cdleme21d  40324  cdleme21e  40325  cdleme21f  40326  cdleme22aa  40333  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f2  40341  cdleme22g  40342  cdleme23b  40344  cdleme26eALTN  40355  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme28a  40364  cdleme28b  40365  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35h  40450  cdleme35sn2aw  40452  cdleme41sn3aw  40468  cdleme41sn4aw  40469  cdlemeg46gfre  40526  cdlemf1  40555  cdlemg1cex  40582  cdlemg2ce  40586  cdlemg4d  40607  cdlemg4e  40608  cdlemg4f  40609  cdlemg4  40611  cdlemg6d  40615  cdlemg6e  40616  cdlemg7fvN  40618  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9b  40627  cdlemg9  40628  cdlemg11aq  40632  cdlemg10a  40634  cdlemg12a  40637  cdlemg12b  40638  cdlemg12c  40639  cdlemg12d  40640  cdlemg13  40646  cdlemg14f  40647  cdlemg14g  40648  cdlemg17b  40656  cdlemg17dN  40657  cdlemg17e  40659  cdlemg17i  40663  cdlemg17pq  40666  cdlemg17iqN  40668  cdlemg18c  40674  cdlemg18d  40675  cdlemg18  40676  cdlemg19  40678  cdlemg21  40680  cdlemg27a  40686  cdlemg31b0N  40688  cdlemg27b  40690  cdlemg31c  40693  cdlemg33b0  40695  cdlemg33c0  40696  cdlemg33  40705  cdlemg35  40707  cdlemg43  40724  cdlemg44a  40725  cdlemg46  40729  cdlemh2  40810  cdlemh  40811  cdlemj1  40815  cdlemk3  40827  cdlemk5  40830  cdlemk6  40831  cdlemki  40835  cdlemksv2  40841  cdlemk12  40844  cdlemk15  40849  cdlemk16  40851  cdlemk18  40862  cdlemk19  40863  cdlemk7u  40864  cdlemk12u  40866  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk20-2N  40886  cdlemk22  40887  cdlemk30  40888  cdlemk31  40890  cdlemk24-3  40897  cdlemkid2  40918  cdlemkfid3N  40919  cdlemk11ta  40923  cdlemkid3N  40927  cdlemk11tc  40939  cdlemk45  40941  cdlemk46  40942  cdlemk47  40943  cdlemk52  40948  cdlemk53a  40949  cdlemk53b  40950  cdleml1N  40970  cdleml3N  40972  cdlemn7  41197  cdlemn10  41200  dihordlem7  41208  dihord1  41212  dihord11c  41218  dihord2  41221  hlhilphllem  41953  fmuldfeq  45581  seposep  48914  iscnrm3rlem8  48935  iscnrm3llem2  48938