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  7315  smogt  8307  frlmphl  21761  mdetuni0  22586  mdetmul  22588  gsummatr01lem3  22622  decpmatmullem  22736  tsmsxp  24120  log2sumbnd  27507  nosupres  27671  noinfres  27686  ax5seg  29007  wlkoniswlk  29728  iocinioc2  32852  totprob  34571  cgrtr  36174  cgrtr3  36176  ofscom  36189  cgrextend  36190  segconeq  36192  ifscgr  36226  btwnxfr  36238  colinearxfr  36257  brofs2  36259  brifs2  36260  fscgr  36262  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem7  36275  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem12  36280  seglecgr12im  36292  seglecgr12  36293  segletr  36296  outsideofeq  36312  ivthALT  36517  lshpkrlem5  39560  lshpkrlem6  39561  exatleN  39850  atbtwn  39892  atbtwnexOLDN  39893  atbtwnex  39894  4noncolr3  39899  3dimlem3a  39906  3dimlem4a  39909  3dim1  39913  3dim2  39914  1cvrat  39922  2atjlej  39925  hlatexch4  39927  ps-2b  39928  2atm  39973  2atmat  40007  4atlem11b  40054  4atlem11  40055  4at  40059  4at2  40060  2lplnja  40065  2lplnj  40066  dalemswapyz  40102  dalemccnedd  40133  cdlemb  40240  paddasslem5  40270  paddasslem15  40280  pmodlem1  40292  dalawlem1  40317  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  osumcllem5N  40406  osumcllem6N  40407  lhpexle3lem  40457  lhpmcvr4N  40472  lhpmcvr6N  40474  4atex2  40523  4atex2-0bOLDN  40525  4atex3  40527  ltrn11at  40593  trlval3  40633  cdlemd3  40646  cdleme0moN  40671  cdleme7aa  40688  cdleme7b  40690  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme16aN  40705  cdleme11dN  40708  cdleme11e  40709  cdleme11l  40715  cdleme11  40716  cdleme12  40717  cdleme14  40719  cdleme15b  40721  cdleme15c  40722  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme17c  40734  cdleme18c  40739  cdleme18d  40741  cdlemeda  40744  cdleme19a  40749  cdleme19b  40750  cdleme19c  40751  cdleme20aN  40755  cdleme20bN  40756  cdleme20d  40758  cdleme20i  40763  cdleme20j  40764  cdleme20l1  40766  cdleme20l2  40767  cdleme21d  40776  cdleme21e  40777  cdleme21f  40778  cdleme22aa  40785  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f2  40793  cdleme22g  40794  cdleme23b  40796  cdleme26eALTN  40807  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme28a  40816  cdleme28b  40817  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35h  40902  cdleme35sn2aw  40904  cdleme41sn3aw  40920  cdleme41sn4aw  40921  cdlemeg46gfre  40978  cdlemf1  41007  cdlemg1cex  41034  cdlemg2ce  41038  cdlemg4d  41059  cdlemg4e  41060  cdlemg4f  41061  cdlemg4  41063  cdlemg6d  41067  cdlemg6e  41068  cdlemg7fvN  41070  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg9b  41079  cdlemg9  41080  cdlemg11aq  41084  cdlemg10a  41086  cdlemg12a  41089  cdlemg12b  41090  cdlemg12c  41091  cdlemg12d  41092  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17b  41108  cdlemg17dN  41109  cdlemg17e  41111  cdlemg17i  41115  cdlemg17pq  41118  cdlemg17iqN  41120  cdlemg18c  41126  cdlemg18d  41127  cdlemg18  41128  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg31b0N  41140  cdlemg27b  41142  cdlemg31c  41145  cdlemg33b0  41147  cdlemg33c0  41148  cdlemg33  41157  cdlemg35  41159  cdlemg43  41176  cdlemg44a  41177  cdlemg46  41181  cdlemh2  41262  cdlemh  41263  cdlemj1  41267  cdlemk3  41279  cdlemk5  41282  cdlemk6  41283  cdlemki  41287  cdlemksv2  41293  cdlemk12  41296  cdlemk15  41301  cdlemk16  41303  cdlemk18  41314  cdlemk19  41315  cdlemk7u  41316  cdlemk12u  41318  cdlemkoatnle-2N  41321  cdlemk13-2N  41322  cdlemkole-2N  41323  cdlemk14-2N  41324  cdlemk15-2N  41325  cdlemk16-2N  41326  cdlemk17-2N  41327  cdlemk18-2N  41332  cdlemk19-2N  41333  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk20-2N  41338  cdlemk22  41339  cdlemk30  41340  cdlemk31  41342  cdlemk24-3  41349  cdlemkid2  41370  cdlemkfid3N  41371  cdlemk11ta  41375  cdlemkid3N  41379  cdlemk11tc  41391  cdlemk45  41393  cdlemk46  41394  cdlemk47  41395  cdlemk52  41400  cdlemk53a  41401  cdlemk53b  41402  cdleml1N  41422  cdleml3N  41424  cdlemn7  41649  cdlemn10  41652  dihordlem7  41660  dihord1  41664  dihord11c  41670  dihord2  41673  hlhilphllem  42405  fmuldfeq  46013  seposep  49401  iscnrm3rlem8  49422  iscnrm3llem2  49425