Theorem simp31 1211

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simp131  1310  simp231  1319  simp331  1328  smogt  8104  frlmphl  20743  mdetuni0  21518  mdetmul  21520  gsummatr01lem3  21554  decpmatmullem  21668  tsmsxp  23052  log2sumbnd  26425  ax5seg  27029  wlkoniswlk  27749  iocinioc2  30820  totprob  32106  eqfunresadj  33454  nosupres  33647  noinfres  33662  cgrtr  34031  cgrtr3  34033  ofscom  34046  cgrextend  34047  segconeq  34049  ifscgr  34083  btwnxfr  34095  colinearxfr  34114  brofs2  34116  brifs2  34117  fscgr  34119  btwnconn1lem1  34126  btwnconn1lem2  34127  btwnconn1lem5  34130  btwnconn1lem6  34131  btwnconn1lem7  34132  btwnconn1lem8  34133  btwnconn1lem9  34134  btwnconn1lem10  34135  btwnconn1lem11  34136  btwnconn1lem12  34137  seglecgr12im  34149  seglecgr12  34150  segletr  34153  outsideofeq  34169  ivthALT  34261  lshpkrlem5  36865  lshpkrlem6  36866  exatleN  37155  atbtwn  37197  atbtwnexOLDN  37198  atbtwnex  37199  4noncolr3  37204  3dimlem3a  37211  3dimlem4a  37214  3dim1  37218  3dim2  37219  1cvrat  37227  2atjlej  37230  hlatexch4  37232  ps-2b  37233  2atm  37278  2atmat  37312  4atlem11b  37359  4atlem11  37360  4at  37364  4at2  37365  2lplnja  37370  2lplnj  37371  dalemswapyz  37407  dalemccnedd  37438  cdlemb  37545  paddasslem5  37575  paddasslem15  37585  pmodlem1  37597  dalawlem1  37622  dalawlem3  37624  dalawlem4  37625  dalawlem5  37626  dalawlem6  37627  dalawlem7  37628  dalawlem8  37629  dalawlem9  37630  dalawlem11  37632  dalawlem12  37633  dalawlem15  37636  osumcllem5N  37711  osumcllem6N  37712  lhpexle3lem  37762  lhpmcvr4N  37777  lhpmcvr6N  37779  4atex2  37828  4atex2-0bOLDN  37830  4atex3  37832  ltrn11at  37898  trlval3  37938  cdlemd3  37951  cdleme0moN  37976  cdleme7aa  37993  cdleme7b  37995  cdleme7c  37996  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme7  38000  cdleme16aN  38010  cdleme11dN  38013  cdleme11e  38014  cdleme11l  38020  cdleme11  38021  cdleme12  38022  cdleme14  38024  cdleme15b  38026  cdleme15c  38027  cdleme16b  38030  cdleme16c  38031  cdleme16d  38032  cdleme16e  38033  cdleme16f  38034  cdleme17c  38039  cdleme18c  38044  cdleme18d  38046  cdlemeda  38049  cdleme19a  38054  cdleme19b  38055  cdleme19c  38056  cdleme20aN  38060  cdleme20bN  38061  cdleme20d  38063  cdleme20i  38068  cdleme20j  38069  cdleme20l1  38071  cdleme20l2  38072  cdleme21d  38081  cdleme21e  38082  cdleme21f  38083  cdleme22aa  38090  cdleme22e  38095  cdleme22eALTN  38096  cdleme22f2  38098  cdleme22g  38099  cdleme23b  38101  cdleme26eALTN  38112  cdleme26fALTN  38113  cdleme26f  38114  cdleme26f2ALTN  38115  cdleme26f2  38116  cdleme28a  38121  cdleme28b  38122  cdleme32b  38193  cdleme32c  38194  cdleme32e  38196  cdleme35h  38207  cdleme35sn2aw  38209  cdleme41sn3aw  38225  cdleme41sn4aw  38226  cdlemeg46gfre  38283  cdlemf1  38312  cdlemg1cex  38339  cdlemg2ce  38343  cdlemg4d  38364  cdlemg4e  38365  cdlemg4f  38366  cdlemg4  38368  cdlemg6d  38372  cdlemg6e  38373  cdlemg7fvN  38375  cdlemg8b  38379  cdlemg8c  38380  cdlemg9a  38383  cdlemg9b  38384  cdlemg9  38385  cdlemg11aq  38389  cdlemg10a  38391  cdlemg12a  38394  cdlemg12b  38395  cdlemg12c  38396  cdlemg12d  38397  cdlemg13  38403  cdlemg14f  38404  cdlemg14g  38405  cdlemg17b  38413  cdlemg17dN  38414  cdlemg17e  38416  cdlemg17i  38420  cdlemg17pq  38423  cdlemg17iqN  38425  cdlemg18c  38431  cdlemg18d  38432  cdlemg18  38433  cdlemg19  38435  cdlemg21  38437  cdlemg27a  38443  cdlemg31b0N  38445  cdlemg27b  38447  cdlemg31c  38450  cdlemg33b0  38452  cdlemg33c0  38453  cdlemg33  38462  cdlemg35  38464  cdlemg43  38481  cdlemg44a  38482  cdlemg46  38486  cdlemh2  38567  cdlemh  38568  cdlemj1  38572  cdlemk3  38584  cdlemk5  38587  cdlemk6  38588  cdlemki  38592  cdlemksv2  38598  cdlemk12  38601  cdlemk15  38606  cdlemk16  38608  cdlemk18  38619  cdlemk19  38620  cdlemk7u  38621  cdlemk12u  38623  cdlemkoatnle-2N  38626  cdlemk13-2N  38627  cdlemkole-2N  38628  cdlemk14-2N  38629  cdlemk15-2N  38630  cdlemk16-2N  38631  cdlemk17-2N  38632  cdlemk18-2N  38637  cdlemk19-2N  38638  cdlemk7u-2N  38639  cdlemk11u-2N  38640  cdlemk12u-2N  38641  cdlemk20-2N  38643  cdlemk22  38644  cdlemk30  38645  cdlemk31  38647  cdlemk24-3  38654  cdlemkid2  38675  cdlemkfid3N  38676  cdlemk11ta  38680  cdlemkid3N  38684  cdlemk11tc  38696  cdlemk45  38698  cdlemk46  38699  cdlemk47  38700  cdlemk52  38705  cdlemk53a  38706  cdlemk53b  38707  cdleml1N  38727  cdleml3N  38729  cdlemn7  38954  cdlemn10  38957  dihordlem7  38965  dihord1  38969  dihord11c  38975  dihord2  38978  hlhilphllem  39710  fmuldfeq  42799  seposep  45892  iscnrm3rlem8  45914  iscnrm3llem2  45917