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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp131  1310  simp231  1319  simp331  1328  eqfunresadj  7308  smogt  8300  frlmphl  21771  mdetuni0  22596  mdetmul  22598  gsummatr01lem3  22632  decpmatmullem  22746  tsmsxp  24130  log2sumbnd  27521  nosupres  27685  noinfres  27700  ax5seg  29021  wlkoniswlk  29743  iocinioc2  32867  totprob  34587  cgrtr  36190  cgrtr3  36192  ofscom  36205  cgrextend  36206  segconeq  36208  ifscgr  36242  btwnxfr  36254  colinearxfr  36273  brofs2  36275  brifs2  36276  fscgr  36278  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  btwnconn1lem8  36292  btwnconn1lem9  36293  btwnconn1lem10  36294  btwnconn1lem11  36295  btwnconn1lem12  36296  seglecgr12im  36308  seglecgr12  36309  segletr  36312  outsideofeq  36328  ivthALT  36533  lshpkrlem5  39574  lshpkrlem6  39575  exatleN  39864  atbtwn  39906  atbtwnexOLDN  39907  atbtwnex  39908  4noncolr3  39913  3dimlem3a  39920  3dimlem4a  39923  3dim1  39927  3dim2  39928  1cvrat  39936  2atjlej  39939  hlatexch4  39941  ps-2b  39942  2atm  39987  2atmat  40021  4atlem11b  40068  4atlem11  40069  4at  40073  4at2  40074  2lplnja  40079  2lplnj  40080  dalemswapyz  40116  dalemccnedd  40147  cdlemb  40254  paddasslem5  40284  paddasslem15  40294  pmodlem1  40306  dalawlem1  40331  dalawlem3  40333  dalawlem4  40334  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem9  40339  dalawlem11  40341  dalawlem12  40342  dalawlem15  40345  osumcllem5N  40420  osumcllem6N  40421  lhpexle3lem  40471  lhpmcvr4N  40486  lhpmcvr6N  40488  4atex2  40537  4atex2-0bOLDN  40539  4atex3  40541  ltrn11at  40607  trlval3  40647  cdlemd3  40660  cdleme0moN  40685  cdleme7aa  40702  cdleme7b  40704  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme16aN  40719  cdleme11dN  40722  cdleme11e  40723  cdleme11l  40729  cdleme11  40730  cdleme12  40731  cdleme14  40733  cdleme15b  40735  cdleme15c  40736  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme17c  40748  cdleme18c  40753  cdleme18d  40755  cdlemeda  40758  cdleme19a  40763  cdleme19b  40764  cdleme19c  40765  cdleme20aN  40769  cdleme20bN  40770  cdleme20d  40772  cdleme20i  40777  cdleme20j  40778  cdleme20l1  40780  cdleme20l2  40781  cdleme21d  40790  cdleme21e  40791  cdleme21f  40792  cdleme22aa  40799  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f2  40807  cdleme22g  40808  cdleme23b  40810  cdleme26eALTN  40821  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme28a  40830  cdleme28b  40831  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35h  40916  cdleme35sn2aw  40918  cdleme41sn3aw  40934  cdleme41sn4aw  40935  cdlemeg46gfre  40992  cdlemf1  41021  cdlemg1cex  41048  cdlemg2ce  41052  cdlemg4d  41073  cdlemg4e  41074  cdlemg4f  41075  cdlemg4  41077  cdlemg6d  41081  cdlemg6e  41082  cdlemg7fvN  41084  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg9  41094  cdlemg11aq  41098  cdlemg10a  41100  cdlemg12a  41103  cdlemg12b  41104  cdlemg12c  41105  cdlemg12d  41106  cdlemg13  41112  cdlemg14f  41113  cdlemg14g  41114  cdlemg17b  41122  cdlemg17dN  41123  cdlemg17e  41125  cdlemg17i  41129  cdlemg17pq  41132  cdlemg17iqN  41134  cdlemg18c  41140  cdlemg18d  41141  cdlemg18  41142  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg31b0N  41154  cdlemg27b  41156  cdlemg31c  41159  cdlemg33b0  41161  cdlemg33c0  41162  cdlemg33  41171  cdlemg35  41173  cdlemg43  41190  cdlemg44a  41191  cdlemg46  41195  cdlemh2  41276  cdlemh  41277  cdlemj1  41281  cdlemk3  41293  cdlemk5  41296  cdlemk6  41297  cdlemki  41301  cdlemksv2  41307  cdlemk12  41310  cdlemk15  41315  cdlemk16  41317  cdlemk18  41328  cdlemk19  41329  cdlemk7u  41330  cdlemk12u  41332  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk20-2N  41352  cdlemk22  41353  cdlemk30  41354  cdlemk31  41356  cdlemk24-3  41363  cdlemkid2  41384  cdlemkfid3N  41385  cdlemk11ta  41389  cdlemkid3N  41393  cdlemk11tc  41405  cdlemk45  41407  cdlemk46  41408  cdlemk47  41409  cdlemk52  41414  cdlemk53a  41415  cdlemk53b  41416  cdleml1N  41436  cdleml3N  41438  cdlemn7  41663  cdlemn10  41666  dihordlem7  41674  dihord1  41678  dihord11c  41684  dihord2  41687  hlhilphllem  42419  fmuldfeq  46031  seposep  49413  iscnrm3rlem8  49434  iscnrm3llem2  49437