Theorem simp32 1229

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp32	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1155	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp132  1328  simp232  1337  simp332  1346  eqfunresadj  7401  smogt  8413  axdc3lem4  10570  bitsfzo  16649  frlmphl  22142  mdetunilem4  22985  mdetuni0  22991  mdetmul  22993  decpmatmullem  23144  logfacbnd3  27607  logexprlim  27609  log2sumbnd  27928  nosupfv  28120  nosupres  28121  noinffv  28135  noinfres  28136  ax5seg  29573  numclwwlk1lem2foa  31012  iocinioc2  33467  totprob  35170  cgrtr  36972  cgrtr3  36974  ofscom  36987  cgrextend  36988  segconeq  36990  ifscgr  37024  colinearxfr  37055  brofs2  37057  brifs2  37058  fscgr  37060  btwnconn1lem2  37068  btwnconn1lem9  37075  btwnconn1lem10  37076  btwnconn1lem11  37077  btwnconn1lem12  37078  brsegle2  37089  seglecgr12im  37090  seglecgr12  37091  segletr  37094  outsideofeq  37110  ivthALT  37338  lshpkrlem5  40437  lshpkrlem6  40438  atbtwnexOLDN  40770  atbtwnex  40771  4noncolr3  40776  3dimlem3a  40783  3dim1  40790  3dim2  40791  1cvrat  40799  2atjlej  40802  hlatexch4  40804  ps-2b  40805  2atm  40850  ps-2c  40851  2atmat  40884  4atlem10  40929  4atlem11b  40931  4atlem11  40932  4at  40936  4at2  40937  2lplnja  40942  2lplnj  40943  dalemswapyz  40979  dalem-ddly  41009  cdlemb  41117  paddasslem5  41147  pmodlem1  41169  dalawlem1  41194  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  osumcllem5N  41283  osumcllem6N  41284  lhpexle3lem  41334  lhpmcvr4N  41349  lhpmcvr6N  41351  4atexlemex6  41397  4atex2  41400  4atex2-0bOLDN  41402  4atex2-0cOLDN  41403  ltrn11at  41470  trlval3  41510  cdlemd3  41523  cdleme7aa  41565  cdleme7b  41567  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme16aN  41582  cdleme11dN  41585  cdleme11e  41586  cdleme11l  41592  cdleme11  41593  cdleme12  41594  cdleme14  41596  cdleme15a  41597  cdleme15c  41599  cdleme16c  41603  cdleme16d  41604  cdleme16e  41605  cdleme16f  41606  cdleme17c  41611  cdleme18c  41616  cdlemeda  41621  cdlemednpq  41622  cdleme19a  41626  cdleme19c  41628  cdleme20aN  41632  cdleme20bN  41633  cdleme20l1  41643  cdleme20l2  41644  cdleme22aa  41662  cdleme22a  41663  cdleme22g  41671  cdleme23b  41673  cdleme23c  41674  cdleme26fALTN  41685  cdleme26f  41686  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme28b  41694  cdleme32b  41765  cdleme32c  41766  cdleme32e  41768  cdleme35h  41779  cdleme35sn2aw  41781  cdleme38m  41786  cdleme40n  41791  cdleme41sn3aw  41797  cdleme41sn4aw  41798  cdlemeg46gfre  41855  cdlemf1  41884  cdlemg1cex  41911  cdlemg2ce  41915  cdlemg4d  41936  cdlemg4  41940  cdlemg7fvN  41947  cdlemg8b  41951  cdlemg8c  41952  cdlemg9a  41955  cdlemg11aq  41961  cdlemg10a  41963  cdlemg12a  41966  cdlemg12b  41967  cdlemg12d  41969  cdlemg12g  41972  cdlemg12  41973  cdlemg13a  41974  cdlemg13  41975  cdlemg14f  41976  cdlemg14g  41977  cdlemg17b  41985  cdlemg17dN  41986  cdlemg17e  41988  cdlemg17pq  41995  cdlemg17iqN  41997  cdlemg18c  42003  cdlemg18d  42004  cdlemg19a  42006  cdlemg19  42007  cdlemg21  42009  cdlemg27a  42015  cdlemg28a  42016  cdlemg31b0N  42017  cdlemg27b  42019  cdlemg31c  42022  cdlemg33b0  42024  cdlemg28  42027  cdlemg33a  42029  cdlemg33  42034  cdlemg35  42036  cdlemg36  42037  cdlemg44a  42054  cdlemg46  42058  cdlemh2  42139  cdlemh  42140  cdlemj1  42144  cdlemk5  42159  cdlemk6  42160  cdlemki  42164  cdlemksv2  42170  cdlemk7  42171  cdlemk11  42172  cdlemkole  42176  cdlemk14  42177  cdlemk16  42180  cdlemk1u  42182  cdlemk18  42191  cdlemk19  42192  cdlemk7u  42193  cdlemk11u  42194  cdlemk33N  42232  cdlemkid2  42247  cdlemkfid3N  42248  cdlemk11ta  42252  cdlemk11tc  42268  cdlemk45  42270  cdlemk46  42271  cdlemk47  42272  cdlemk52  42277  cdlemk53a  42278  cdlemk54  42281  cdlemk55a  42282  cdleml1N  42299  cdleml3N  42301  cdlemn7  42526  cdlemn8  42527  cdlemn10  42529  dihordlem7  42537  dihordlem7b  42538  dihord1  42541  dihord10  42546  dihord11c  42547  dihord2  42550  hlhilphllem  43282  fmuldfeq  46868  seposep  50371  iscnrm3rlem8  50392  iscnrm3llem2  50395