Theorem simp31 1259

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpl31OLD  1335  simpr31OLD  1353  simp131  1400  simp231  1409  simp331  1418  smogt  7709  frlmphl  20350  mdetuni0  20658  mdetmul  20660  gsummatr01lem3  20695  decpmatmullem  20809  tsmsxp  22191  log2sumbnd  25469  ax5seg  26054  wlkoniswlk  26807  iocinioc2  29890  totprob  30836  eqfunresadj  32002  nosupres  32195  cgrtr  32441  cgrtr3  32443  ofscom  32456  cgrextend  32457  segconeq  32459  ifscgr  32493  btwnxfr  32505  colinearxfr  32524  brofs2  32526  brifs2  32527  fscgr  32529  btwnconn1lem1  32536  btwnconn1lem2  32537  btwnconn1lem5  32540  btwnconn1lem6  32541  btwnconn1lem7  32542  btwnconn1lem8  32543  btwnconn1lem9  32544  btwnconn1lem10  32545  btwnconn1lem11  32546  btwnconn1lem12  32547  seglecgr12im  32559  seglecgr12  32560  segletr  32563  outsideofeq  32579  ivthALT  32672  lshpkrlem5  34912  lshpkrlem6  34913  exatleN  35202  atbtwn  35244  atbtwnexOLDN  35245  atbtwnex  35246  4noncolr3  35251  3dimlem3a  35258  3dimlem4a  35261  3dim1  35265  3dim2  35266  1cvrat  35274  2atjlej  35277  hlatexch4  35279  ps-2b  35280  2atm  35325  2atmat  35359  4atlem11b  35406  4atlem11  35407  4at  35411  4at2  35412  2lplnja  35417  2lplnj  35418  dalemswapyz  35454  dalemccnedd  35485  cdlemb  35592  paddasslem5  35622  paddasslem15  35632  pmodlem1  35644  dalawlem1  35669  dalawlem3  35671  dalawlem4  35672  dalawlem5  35673  dalawlem6  35674  dalawlem7  35675  dalawlem8  35676  dalawlem9  35677  dalawlem11  35679  dalawlem12  35680  dalawlem15  35683  osumcllem5N  35758  osumcllem6N  35759  lhpexle3lem  35809  lhpmcvr4N  35824  lhpmcvr6N  35826  4atex2  35875  4atex2-0bOLDN  35877  4atex3  35879  ltrn11at  35945  trlval3  35985  cdlemd3  35998  cdleme0moN  36023  cdleme7aa  36040  cdleme7b  36042  cdleme7c  36043  cdleme7d  36044  cdleme7e  36045  cdleme7ga  36046  cdleme7  36047  cdleme16aN  36057  cdleme11dN  36060  cdleme11e  36061  cdleme11l  36067  cdleme11  36068  cdleme12  36069  cdleme14  36071  cdleme15b  36073  cdleme15c  36074  cdleme16b  36077  cdleme16c  36078  cdleme16d  36079  cdleme16e  36080  cdleme16f  36081  cdleme17c  36086  cdleme18c  36091  cdleme18d  36093  cdlemeda  36096  cdleme19a  36101  cdleme19b  36102  cdleme19c  36103  cdleme20aN  36107  cdleme20bN  36108  cdleme20d  36110  cdleme20i  36115  cdleme20j  36116  cdleme20l1  36118  cdleme20l2  36119  cdleme21d  36128  cdleme21e  36129  cdleme21f  36130  cdleme22aa  36137  cdleme22e  36142  cdleme22eALTN  36143  cdleme22f2  36145  cdleme22g  36146  cdleme23b  36148  cdleme26eALTN  36159  cdleme26fALTN  36160  cdleme26f  36161  cdleme26f2ALTN  36162  cdleme26f2  36163  cdleme28a  36168  cdleme28b  36169  cdleme32b  36240  cdleme32c  36241  cdleme32e  36243  cdleme35h  36254  cdleme35sn2aw  36256  cdleme41sn3aw  36272  cdleme41sn4aw  36273  cdlemeg46gfre  36330  cdlemf1  36359  cdlemg1cex  36386  cdlemg2ce  36390  cdlemg4d  36411  cdlemg4e  36412  cdlemg4f  36413  cdlemg4  36415  cdlemg6d  36419  cdlemg6e  36420  cdlemg7fvN  36422  cdlemg8b  36426  cdlemg8c  36427  cdlemg9a  36430  cdlemg9b  36431  cdlemg9  36432  cdlemg11aq  36436  cdlemg10a  36438  cdlemg12a  36441  cdlemg12b  36442  cdlemg12c  36443  cdlemg12d  36444  cdlemg13  36450  cdlemg14f  36451  cdlemg14g  36452  cdlemg17b  36460  cdlemg17dN  36461  cdlemg17e  36463  cdlemg17i  36467  cdlemg17pq  36470  cdlemg17iqN  36472  cdlemg18c  36478  cdlemg18d  36479  cdlemg18  36480  cdlemg19  36482  cdlemg21  36484  cdlemg27a  36490  cdlemg31b0N  36492  cdlemg27b  36494  cdlemg31c  36497  cdlemg33b0  36499  cdlemg33c0  36500  cdlemg33  36509  cdlemg35  36511  cdlemg43  36528  cdlemg44a  36529  cdlemg46  36533  cdlemh2  36614  cdlemh  36615  cdlemj1  36619  cdlemk3  36631  cdlemk5  36634  cdlemk6  36635  cdlemki  36639  cdlemksv2  36645  cdlemk12  36648  cdlemk15  36653  cdlemk16  36655  cdlemk18  36666  cdlemk19  36667  cdlemk7u  36668  cdlemk12u  36670  cdlemkoatnle-2N  36673  cdlemk13-2N  36674  cdlemkole-2N  36675  cdlemk14-2N  36676  cdlemk15-2N  36677  cdlemk16-2N  36678  cdlemk17-2N  36679  cdlemk18-2N  36684  cdlemk19-2N  36685  cdlemk7u-2N  36686  cdlemk11u-2N  36687  cdlemk12u-2N  36688  cdlemk20-2N  36690  cdlemk22  36691  cdlemk30  36692  cdlemk31  36694  cdlemk24-3  36701  cdlemkid2  36722  cdlemkfid3N  36723  cdlemk11ta  36727  cdlemkid3N  36731  cdlemk11tc  36743  cdlemk45  36745  cdlemk46  36746  cdlemk47  36747  cdlemk52  36752  cdlemk53a  36753  cdlemk53b  36754  cdleml1N  36774  cdleml3N  36776  cdlemn7  37001  cdlemn10  37004  dihordlem7  37012  dihord1  37016  dihord11c  37022  dihord2  37025  hlhilphllem  37757  fmuldfeq  40312