Theorem simp32 1211

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp132  1310  simp232  1319  simp332  1328  eqfunresadj  7306  smogt  8299  axdc3lem4  10363  bitsfzo  16362  frlmphl  21736  mdetunilem4  22559  mdetuni0  22565  mdetmul  22567  decpmatmullem  22715  logfacbnd3  27190  logexprlim  27192  log2sumbnd  27511  nosupfv  27674  nosupres  27675  noinffv  27689  noinfres  27690  ax5seg  29011  numclwwlk1lem2foa  30429  iocinioc2  32859  totprob  34584  cgrtr  36186  cgrtr3  36188  ofscom  36201  cgrextend  36202  segconeq  36204  ifscgr  36238  colinearxfr  36269  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem2  36282  btwnconn1lem9  36289  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem12  36292  brsegle2  36303  seglecgr12im  36304  seglecgr12  36305  segletr  36308  outsideofeq  36324  ivthALT  36529  lshpkrlem5  39374  lshpkrlem6  39375  atbtwnexOLDN  39707  atbtwnex  39708  4noncolr3  39713  3dimlem3a  39720  3dim1  39727  3dim2  39728  1cvrat  39736  2atjlej  39739  hlatexch4  39741  ps-2b  39742  2atm  39787  ps-2c  39788  2atmat  39821  4atlem10  39866  4atlem11b  39868  4atlem11  39869  4at  39873  4at2  39874  2lplnja  39879  2lplnj  39880  dalemswapyz  39916  dalem-ddly  39946  cdlemb  40054  paddasslem5  40084  pmodlem1  40106  dalawlem1  40131  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem11  40141  dalawlem12  40142  dalawlem15  40145  osumcllem5N  40220  osumcllem6N  40221  lhpexle3lem  40271  lhpmcvr4N  40286  lhpmcvr6N  40288  4atexlemex6  40334  4atex2  40337  4atex2-0bOLDN  40339  4atex2-0cOLDN  40340  ltrn11at  40407  trlval3  40447  cdlemd3  40460  cdleme7aa  40502  cdleme7b  40504  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme7ga  40508  cdleme7  40509  cdleme16aN  40519  cdleme11dN  40522  cdleme11e  40523  cdleme11l  40529  cdleme11  40530  cdleme12  40531  cdleme14  40533  cdleme15a  40534  cdleme15c  40536  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme17c  40548  cdleme18c  40553  cdlemeda  40558  cdlemednpq  40559  cdleme19a  40563  cdleme19c  40565  cdleme20aN  40569  cdleme20bN  40570  cdleme20l1  40580  cdleme20l2  40581  cdleme22aa  40599  cdleme22a  40600  cdleme22g  40608  cdleme23b  40610  cdleme23c  40611  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme28b  40631  cdleme32b  40702  cdleme32c  40703  cdleme32e  40705  cdleme35h  40716  cdleme35sn2aw  40718  cdleme38m  40723  cdleme40n  40728  cdleme41sn3aw  40734  cdleme41sn4aw  40735  cdlemeg46gfre  40792  cdlemf1  40821  cdlemg1cex  40848  cdlemg2ce  40852  cdlemg4d  40873  cdlemg4  40877  cdlemg7fvN  40884  cdlemg8b  40888  cdlemg8c  40889  cdlemg9a  40892  cdlemg11aq  40898  cdlemg10a  40900  cdlemg12a  40903  cdlemg12b  40904  cdlemg12d  40906  cdlemg12g  40909  cdlemg12  40910  cdlemg13a  40911  cdlemg13  40912  cdlemg14f  40913  cdlemg14g  40914  cdlemg17b  40922  cdlemg17dN  40923  cdlemg17e  40925  cdlemg17pq  40932  cdlemg17iqN  40934  cdlemg18c  40940  cdlemg18d  40941  cdlemg19a  40943  cdlemg19  40944  cdlemg21  40946  cdlemg27a  40952  cdlemg28a  40953  cdlemg31b0N  40954  cdlemg27b  40956  cdlemg31c  40959  cdlemg33b0  40961  cdlemg28  40964  cdlemg33a  40966  cdlemg33  40971  cdlemg35  40973  cdlemg36  40974  cdlemg44a  40991  cdlemg46  40995  cdlemh2  41076  cdlemh  41077  cdlemj1  41081  cdlemk5  41096  cdlemk6  41097  cdlemki  41101  cdlemksv2  41107  cdlemk7  41108  cdlemk11  41109  cdlemkole  41113  cdlemk14  41114  cdlemk16  41117  cdlemk1u  41119  cdlemk18  41128  cdlemk19  41129  cdlemk7u  41130  cdlemk11u  41131  cdlemk33N  41169  cdlemkid2  41184  cdlemkfid3N  41185  cdlemk11ta  41189  cdlemk11tc  41205  cdlemk45  41207  cdlemk46  41208  cdlemk47  41209  cdlemk52  41214  cdlemk53a  41215  cdlemk54  41218  cdlemk55a  41219  cdleml1N  41236  cdleml3N  41238  cdlemn7  41463  cdlemn8  41464  cdlemn10  41466  dihordlem7  41474  dihordlem7b  41475  dihord1  41478  dihord10  41483  dihord11c  41484  dihord2  41487  hlhilphllem  42219  fmuldfeq  45829  seposep  49171  iscnrm3rlem8  49192  iscnrm3llem2  49195