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  7303  smogt  8296  frlmphl  21727  mdetuni0  22556  mdetmul  22558  gsummatr01lem3  22592  decpmatmullem  22706  tsmsxp  24090  log2sumbnd  27502  nosupres  27666  noinfres  27681  ax5seg  28937  wlkoniswlk  29659  iocinioc2  32787  totprob  34512  cgrtr  36108  cgrtr3  36110  ofscom  36123  cgrextend  36124  segconeq  36126  ifscgr  36160  btwnxfr  36172  colinearxfr  36191  brofs2  36193  brifs2  36194  fscgr  36196  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem5  36207  btwnconn1lem6  36208  btwnconn1lem7  36209  btwnconn1lem8  36210  btwnconn1lem9  36211  btwnconn1lem10  36212  btwnconn1lem11  36213  btwnconn1lem12  36214  seglecgr12im  36226  seglecgr12  36227  segletr  36230  outsideofeq  36246  ivthALT  36451  lshpkrlem5  39286  lshpkrlem6  39287  exatleN  39576  atbtwn  39618  atbtwnexOLDN  39619  atbtwnex  39620  4noncolr3  39625  3dimlem3a  39632  3dimlem4a  39635  3dim1  39639  3dim2  39640  1cvrat  39648  2atjlej  39651  hlatexch4  39653  ps-2b  39654  2atm  39699  2atmat  39733  4atlem11b  39780  4atlem11  39781  4at  39785  4at2  39786  2lplnja  39791  2lplnj  39792  dalemswapyz  39828  dalemccnedd  39859  cdlemb  39966  paddasslem5  39996  paddasslem15  40006  pmodlem1  40018  dalawlem1  40043  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem15  40057  osumcllem5N  40132  osumcllem6N  40133  lhpexle3lem  40183  lhpmcvr4N  40198  lhpmcvr6N  40200  4atex2  40249  4atex2-0bOLDN  40251  4atex3  40253  ltrn11at  40319  trlval3  40359  cdlemd3  40372  cdleme0moN  40397  cdleme7aa  40414  cdleme7b  40416  cdleme7c  40417  cdleme7d  40418  cdleme7e  40419  cdleme7ga  40420  cdleme7  40421  cdleme16aN  40431  cdleme11dN  40434  cdleme11e  40435  cdleme11l  40441  cdleme11  40442  cdleme12  40443  cdleme14  40445  cdleme15b  40447  cdleme15c  40448  cdleme16b  40451  cdleme16c  40452  cdleme16d  40453  cdleme16e  40454  cdleme16f  40455  cdleme17c  40460  cdleme18c  40465  cdleme18d  40467  cdlemeda  40470  cdleme19a  40475  cdleme19b  40476  cdleme19c  40477  cdleme20aN  40481  cdleme20bN  40482  cdleme20d  40484  cdleme20i  40489  cdleme20j  40490  cdleme20l1  40492  cdleme20l2  40493  cdleme21d  40502  cdleme21e  40503  cdleme21f  40504  cdleme22aa  40511  cdleme22e  40516  cdleme22eALTN  40517  cdleme22f2  40519  cdleme22g  40520  cdleme23b  40522  cdleme26eALTN  40533  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme28a  40542  cdleme28b  40543  cdleme32b  40614  cdleme32c  40615  cdleme32e  40617  cdleme35h  40628  cdleme35sn2aw  40630  cdleme41sn3aw  40646  cdleme41sn4aw  40647  cdlemeg46gfre  40704  cdlemf1  40733  cdlemg1cex  40760  cdlemg2ce  40764  cdlemg4d  40785  cdlemg4e  40786  cdlemg4f  40787  cdlemg4  40789  cdlemg6d  40793  cdlemg6e  40794  cdlemg7fvN  40796  cdlemg8b  40800  cdlemg8c  40801  cdlemg9a  40804  cdlemg9b  40805  cdlemg9  40806  cdlemg11aq  40810  cdlemg10a  40812  cdlemg12a  40815  cdlemg12b  40816  cdlemg12c  40817  cdlemg12d  40818  cdlemg13  40824  cdlemg14f  40825  cdlemg14g  40826  cdlemg17b  40834  cdlemg17dN  40835  cdlemg17e  40837  cdlemg17i  40841  cdlemg17pq  40844  cdlemg17iqN  40846  cdlemg18c  40852  cdlemg18d  40853  cdlemg18  40854  cdlemg19  40856  cdlemg21  40858  cdlemg27a  40864  cdlemg31b0N  40866  cdlemg27b  40868  cdlemg31c  40871  cdlemg33b0  40873  cdlemg33c0  40874  cdlemg33  40883  cdlemg35  40885  cdlemg43  40902  cdlemg44a  40903  cdlemg46  40907  cdlemh2  40988  cdlemh  40989  cdlemj1  40993  cdlemk3  41005  cdlemk5  41008  cdlemk6  41009  cdlemki  41013  cdlemksv2  41019  cdlemk12  41022  cdlemk15  41027  cdlemk16  41029  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk12u  41044  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk7u-2N  41060  cdlemk11u-2N  41061  cdlemk12u-2N  41062  cdlemk20-2N  41064  cdlemk22  41065  cdlemk30  41066  cdlemk31  41068  cdlemk24-3  41075  cdlemkid2  41096  cdlemkfid3N  41097  cdlemk11ta  41101  cdlemkid3N  41105  cdlemk11tc  41117  cdlemk45  41119  cdlemk46  41120  cdlemk47  41121  cdlemk52  41126  cdlemk53a  41127  cdlemk53b  41128  cdleml1N  41148  cdleml3N  41150  cdlemn7  41375  cdlemn10  41378  dihordlem7  41386  dihord1  41390  dihord11c  41396  dihord2  41399  hlhilphllem  42131  fmuldfeq  45745  seposep  49087  iscnrm3rlem8  49108  iscnrm3llem2  49111