Theorem simp31 1206

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp131  1305  simp231  1314  simp331  1323  eqfunresadj  7367  smogt  8388  frlmphl  21749  mdetuni0  22584  mdetmul  22586  gsummatr01lem3  22620  decpmatmullem  22734  tsmsxp  24120  log2sumbnd  27542  nosupres  27706  noinfres  27721  ax5seg  28841  wlkoniswlk  29567  iocinioc2  32649  totprob  34198  cgrtr  35739  cgrtr3  35741  ofscom  35754  cgrextend  35755  segconeq  35757  ifscgr  35791  btwnxfr  35803  colinearxfr  35822  brofs2  35824  brifs2  35825  fscgr  35827  btwnconn1lem1  35834  btwnconn1lem2  35835  btwnconn1lem5  35838  btwnconn1lem6  35839  btwnconn1lem7  35840  btwnconn1lem8  35841  btwnconn1lem9  35842  btwnconn1lem10  35843  btwnconn1lem11  35844  btwnconn1lem12  35845  seglecgr12im  35857  seglecgr12  35858  segletr  35861  outsideofeq  35877  ivthALT  35970  lshpkrlem5  38736  lshpkrlem6  38737  exatleN  39027  atbtwn  39069  atbtwnexOLDN  39070  atbtwnex  39071  4noncolr3  39076  3dimlem3a  39083  3dimlem4a  39086  3dim1  39090  3dim2  39091  1cvrat  39099  2atjlej  39102  hlatexch4  39104  ps-2b  39105  2atm  39150  2atmat  39184  4atlem11b  39231  4atlem11  39232  4at  39236  4at2  39237  2lplnja  39242  2lplnj  39243  dalemswapyz  39279  dalemccnedd  39310  cdlemb  39417  paddasslem5  39447  paddasslem15  39457  pmodlem1  39469  dalawlem1  39494  dalawlem3  39496  dalawlem4  39497  dalawlem5  39498  dalawlem6  39499  dalawlem7  39500  dalawlem8  39501  dalawlem9  39502  dalawlem11  39504  dalawlem12  39505  dalawlem15  39508  osumcllem5N  39583  osumcllem6N  39584  lhpexle3lem  39634  lhpmcvr4N  39649  lhpmcvr6N  39651  4atex2  39700  4atex2-0bOLDN  39702  4atex3  39704  ltrn11at  39770  trlval3  39810  cdlemd3  39823  cdleme0moN  39848  cdleme7aa  39865  cdleme7b  39867  cdleme7c  39868  cdleme7d  39869  cdleme7e  39870  cdleme7ga  39871  cdleme7  39872  cdleme16aN  39882  cdleme11dN  39885  cdleme11e  39886  cdleme11l  39892  cdleme11  39893  cdleme12  39894  cdleme14  39896  cdleme15b  39898  cdleme15c  39899  cdleme16b  39902  cdleme16c  39903  cdleme16d  39904  cdleme16e  39905  cdleme16f  39906  cdleme17c  39911  cdleme18c  39916  cdleme18d  39918  cdlemeda  39921  cdleme19a  39926  cdleme19b  39927  cdleme19c  39928  cdleme20aN  39932  cdleme20bN  39933  cdleme20d  39935  cdleme20i  39940  cdleme20j  39941  cdleme20l1  39943  cdleme20l2  39944  cdleme21d  39953  cdleme21e  39954  cdleme21f  39955  cdleme22aa  39962  cdleme22e  39967  cdleme22eALTN  39968  cdleme22f2  39970  cdleme22g  39971  cdleme23b  39973  cdleme26eALTN  39984  cdleme26fALTN  39985  cdleme26f  39986  cdleme26f2ALTN  39987  cdleme26f2  39988  cdleme28a  39993  cdleme28b  39994  cdleme32b  40065  cdleme32c  40066  cdleme32e  40068  cdleme35h  40079  cdleme35sn2aw  40081  cdleme41sn3aw  40097  cdleme41sn4aw  40098  cdlemeg46gfre  40155  cdlemf1  40184  cdlemg1cex  40211  cdlemg2ce  40215  cdlemg4d  40236  cdlemg4e  40237  cdlemg4f  40238  cdlemg4  40240  cdlemg6d  40244  cdlemg6e  40245  cdlemg7fvN  40247  cdlemg8b  40251  cdlemg8c  40252  cdlemg9a  40255  cdlemg9b  40256  cdlemg9  40257  cdlemg11aq  40261  cdlemg10a  40263  cdlemg12a  40266  cdlemg12b  40267  cdlemg12c  40268  cdlemg12d  40269  cdlemg13  40275  cdlemg14f  40276  cdlemg14g  40277  cdlemg17b  40285  cdlemg17dN  40286  cdlemg17e  40288  cdlemg17i  40292  cdlemg17pq  40295  cdlemg17iqN  40297  cdlemg18c  40303  cdlemg18d  40304  cdlemg18  40305  cdlemg19  40307  cdlemg21  40309  cdlemg27a  40315  cdlemg31b0N  40317  cdlemg27b  40319  cdlemg31c  40322  cdlemg33b0  40324  cdlemg33c0  40325  cdlemg33  40334  cdlemg35  40336  cdlemg43  40353  cdlemg44a  40354  cdlemg46  40358  cdlemh2  40439  cdlemh  40440  cdlemj1  40444  cdlemk3  40456  cdlemk5  40459  cdlemk6  40460  cdlemki  40464  cdlemksv2  40470  cdlemk12  40473  cdlemk15  40478  cdlemk16  40480  cdlemk18  40491  cdlemk19  40492  cdlemk7u  40493  cdlemk12u  40495  cdlemkoatnle-2N  40498  cdlemk13-2N  40499  cdlemkole-2N  40500  cdlemk14-2N  40501  cdlemk15-2N  40502  cdlemk16-2N  40503  cdlemk17-2N  40504  cdlemk18-2N  40509  cdlemk19-2N  40510  cdlemk7u-2N  40511  cdlemk11u-2N  40512  cdlemk12u-2N  40513  cdlemk20-2N  40515  cdlemk22  40516  cdlemk30  40517  cdlemk31  40519  cdlemk24-3  40526  cdlemkid2  40547  cdlemkfid3N  40548  cdlemk11ta  40552  cdlemkid3N  40556  cdlemk11tc  40568  cdlemk45  40570  cdlemk46  40571  cdlemk47  40572  cdlemk52  40577  cdlemk53a  40578  cdlemk53b  40579  cdleml1N  40599  cdleml3N  40601  cdlemn7  40826  cdlemn10  40829  dihordlem7  40837  dihord1  40841  dihord11c  40847  dihord2  40850  hlhilphllem  41586  fmuldfeq  45114  seposep  48135  iscnrm3rlem8  48157  iscnrm3llem2  48160