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 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simp131  1327  simp231  1336  simp331  1345  eqfunresadj  7358  smogt  8350  frlmphl  21931  mdetuni0  22778  mdetmul  22780  gsummatr01lem3  22814  decpmatmullem  22928  tsmsxp  24312  log2sumbnd  27708  nosupres  27871  noinfres  27886  ax5seg  29288  wlkoniswlk  30009  iocinioc2  33124  totprob  34817  cgrtr  36484  cgrtr3  36486  ofscom  36499  cgrextend  36500  segconeq  36502  ifscgr  36536  btwnxfr  36548  colinearxfr  36567  brofs2  36569  brifs2  36570  fscgr  36572  btwnconn1lem1  36579  btwnconn1lem2  36580  btwnconn1lem5  36583  btwnconn1lem6  36584  btwnconn1lem7  36585  btwnconn1lem8  36586  btwnconn1lem9  36587  btwnconn1lem10  36588  btwnconn1lem11  36589  btwnconn1lem12  36590  seglecgr12im  36602  seglecgr12  36603  segletr  36606  outsideofeq  36622  ivthALT  36846  lshpkrlem5  39888  lshpkrlem6  39889  exatleN  40178  atbtwn  40220  atbtwnexOLDN  40221  atbtwnex  40222  4noncolr3  40227  3dimlem3a  40234  3dimlem4a  40237  3dim1  40241  3dim2  40242  1cvrat  40250  2atjlej  40253  hlatexch4  40255  ps-2b  40256  2atm  40301  2atmat  40335  4atlem11b  40382  4atlem11  40383  4at  40387  4at2  40388  2lplnja  40393  2lplnj  40394  dalemswapyz  40430  dalemccnedd  40461  cdlemb  40568  paddasslem5  40598  paddasslem15  40608  pmodlem1  40620  dalawlem1  40645  dalawlem3  40647  dalawlem4  40648  dalawlem5  40649  dalawlem6  40650  dalawlem7  40651  dalawlem8  40652  dalawlem9  40653  dalawlem11  40655  dalawlem12  40656  dalawlem15  40659  osumcllem5N  40734  osumcllem6N  40735  lhpexle3lem  40785  lhpmcvr4N  40800  lhpmcvr6N  40802  4atex2  40851  4atex2-0bOLDN  40853  4atex3  40855  ltrn11at  40921  trlval3  40961  cdlemd3  40974  cdleme0moN  40999  cdleme7aa  41016  cdleme7b  41018  cdleme7c  41019  cdleme7d  41020  cdleme7e  41021  cdleme7ga  41022  cdleme7  41023  cdleme16aN  41033  cdleme11dN  41036  cdleme11e  41037  cdleme11l  41043  cdleme11  41044  cdleme12  41045  cdleme14  41047  cdleme15b  41049  cdleme15c  41050  cdleme16b  41053  cdleme16c  41054  cdleme16d  41055  cdleme16e  41056  cdleme16f  41057  cdleme17c  41062  cdleme18c  41067  cdleme18d  41069  cdlemeda  41072  cdleme19a  41077  cdleme19b  41078  cdleme19c  41079  cdleme20aN  41083  cdleme20bN  41084  cdleme20d  41086  cdleme20i  41091  cdleme20j  41092  cdleme20l1  41094  cdleme20l2  41095  cdleme21d  41104  cdleme21e  41105  cdleme21f  41106  cdleme22aa  41113  cdleme22e  41118  cdleme22eALTN  41119  cdleme22f2  41121  cdleme22g  41122  cdleme23b  41124  cdleme26eALTN  41135  cdleme26fALTN  41136  cdleme26f  41137  cdleme26f2ALTN  41138  cdleme26f2  41139  cdleme28a  41144  cdleme28b  41145  cdleme32b  41216  cdleme32c  41217  cdleme32e  41219  cdleme35h  41230  cdleme35sn2aw  41232  cdleme41sn3aw  41248  cdleme41sn4aw  41249  cdlemeg46gfre  41306  cdlemf1  41335  cdlemg1cex  41362  cdlemg2ce  41366  cdlemg4d  41387  cdlemg4e  41388  cdlemg4f  41389  cdlemg4  41391  cdlemg6d  41395  cdlemg6e  41396  cdlemg7fvN  41398  cdlemg8b  41402  cdlemg8c  41403  cdlemg9a  41406  cdlemg9b  41407  cdlemg9  41408  cdlemg11aq  41412  cdlemg10a  41414  cdlemg12a  41417  cdlemg12b  41418  cdlemg12c  41419  cdlemg12d  41420  cdlemg13  41426  cdlemg14f  41427  cdlemg14g  41428  cdlemg17b  41436  cdlemg17dN  41437  cdlemg17e  41439  cdlemg17i  41443  cdlemg17pq  41446  cdlemg17iqN  41448  cdlemg18c  41454  cdlemg18d  41455  cdlemg18  41456  cdlemg19  41458  cdlemg21  41460  cdlemg27a  41466  cdlemg31b0N  41468  cdlemg27b  41470  cdlemg31c  41473  cdlemg33b0  41475  cdlemg33c0  41476  cdlemg33  41485  cdlemg35  41487  cdlemg43  41504  cdlemg44a  41505  cdlemg46  41509  cdlemh2  41590  cdlemh  41591  cdlemj1  41595  cdlemk3  41607  cdlemk5  41610  cdlemk6  41611  cdlemki  41615  cdlemksv2  41621  cdlemk12  41624  cdlemk15  41629  cdlemk16  41631  cdlemk18  41642  cdlemk19  41643  cdlemk7u  41644  cdlemk12u  41646  cdlemkoatnle-2N  41649  cdlemk13-2N  41650  cdlemkole-2N  41651  cdlemk14-2N  41652  cdlemk15-2N  41653  cdlemk16-2N  41654  cdlemk17-2N  41655  cdlemk18-2N  41660  cdlemk19-2N  41661  cdlemk7u-2N  41662  cdlemk11u-2N  41663  cdlemk12u-2N  41664  cdlemk20-2N  41666  cdlemk22  41667  cdlemk30  41668  cdlemk31  41670  cdlemk24-3  41677  cdlemkid2  41698  cdlemkfid3N  41699  cdlemk11ta  41703  cdlemkid3N  41707  cdlemk11tc  41719  cdlemk45  41721  cdlemk46  41722  cdlemk47  41723  cdlemk52  41728  cdlemk53a  41729  cdlemk53b  41730  cdleml1N  41750  cdleml3N  41752  cdlemn7  41977  cdlemn10  41980  dihordlem7  41988  dihord1  41992  dihord11c  41998  dihord2  42001  hlhilphllem  42733  fmuldfeq  46299  seposep  49704  iscnrm3rlem8  49725  iscnrm3llem2  49728