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  7363  smogt  8356  axdc3lem4  10455  bitsfzo  16525  frlmphl  21994  mdetunilem4  22837  mdetuni0  22843  mdetmul  22845  decpmatmullem  22996  logfacbnd3  27459  logexprlim  27461  log2sumbnd  27780  nosupfv  27942  nosupres  27943  noinffv  27957  noinfres  27958  ax5seg  29395  numclwwlk1lem2foa  30834  iocinioc2  33250  totprob  34938  cgrtr  36572  cgrtr3  36574  ofscom  36587  cgrextend  36588  segconeq  36590  ifscgr  36624  colinearxfr  36655  brofs2  36657  brifs2  36658  fscgr  36660  btwnconn1lem2  36668  btwnconn1lem9  36675  btwnconn1lem10  36676  btwnconn1lem11  36677  btwnconn1lem12  36678  brsegle2  36689  seglecgr12im  36690  seglecgr12  36691  segletr  36694  outsideofeq  36710  ivthALT  36954  lshpkrlem5  39987  lshpkrlem6  39988  atbtwnexOLDN  40320  atbtwnex  40321  4noncolr3  40326  3dimlem3a  40333  3dim1  40340  3dim2  40341  1cvrat  40349  2atjlej  40352  hlatexch4  40354  ps-2b  40355  2atm  40400  ps-2c  40401  2atmat  40434  4atlem10  40479  4atlem11b  40481  4atlem11  40482  4at  40486  4at2  40487  2lplnja  40492  2lplnj  40493  dalemswapyz  40529  dalem-ddly  40559  cdlemb  40667  paddasslem5  40697  pmodlem1  40719  dalawlem1  40744  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem15  40758  osumcllem5N  40833  osumcllem6N  40834  lhpexle3lem  40884  lhpmcvr4N  40899  lhpmcvr6N  40901  4atexlemex6  40947  4atex2  40950  4atex2-0bOLDN  40952  4atex2-0cOLDN  40953  ltrn11at  41020  trlval3  41060  cdlemd3  41073  cdleme7aa  41115  cdleme7b  41117  cdleme7c  41118  cdleme7d  41119  cdleme7e  41120  cdleme7ga  41121  cdleme7  41122  cdleme16aN  41132  cdleme11dN  41135  cdleme11e  41136  cdleme11l  41142  cdleme11  41143  cdleme12  41144  cdleme14  41146  cdleme15a  41147  cdleme15c  41149  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme17c  41161  cdleme18c  41166  cdlemeda  41171  cdlemednpq  41172  cdleme19a  41176  cdleme19c  41178  cdleme20aN  41182  cdleme20bN  41183  cdleme20l1  41193  cdleme20l2  41194  cdleme22aa  41212  cdleme22a  41213  cdleme22g  41221  cdleme23b  41223  cdleme23c  41224  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme28b  41244  cdleme32b  41315  cdleme32c  41316  cdleme32e  41318  cdleme35h  41329  cdleme35sn2aw  41331  cdleme38m  41336  cdleme40n  41341  cdleme41sn3aw  41347  cdleme41sn4aw  41348  cdlemeg46gfre  41405  cdlemf1  41434  cdlemg1cex  41461  cdlemg2ce  41465  cdlemg4d  41486  cdlemg4  41490  cdlemg7fvN  41497  cdlemg8b  41501  cdlemg8c  41502  cdlemg9a  41505  cdlemg11aq  41511  cdlemg10a  41513  cdlemg12a  41516  cdlemg12b  41517  cdlemg12d  41519  cdlemg12g  41522  cdlemg12  41523  cdlemg13a  41524  cdlemg13  41525  cdlemg14f  41526  cdlemg14g  41527  cdlemg17b  41535  cdlemg17dN  41536  cdlemg17e  41538  cdlemg17pq  41545  cdlemg17iqN  41547  cdlemg18c  41553  cdlemg18d  41554  cdlemg19a  41556  cdlemg19  41557  cdlemg21  41559  cdlemg27a  41565  cdlemg28a  41566  cdlemg31b0N  41567  cdlemg27b  41569  cdlemg31c  41572  cdlemg33b0  41574  cdlemg28  41577  cdlemg33a  41579  cdlemg33  41584  cdlemg35  41586  cdlemg36  41587  cdlemg44a  41604  cdlemg46  41608  cdlemh2  41689  cdlemh  41690  cdlemj1  41694  cdlemk5  41709  cdlemk6  41710  cdlemki  41714  cdlemksv2  41720  cdlemk7  41721  cdlemk11  41722  cdlemkole  41726  cdlemk14  41727  cdlemk16  41730  cdlemk1u  41732  cdlemk18  41741  cdlemk19  41742  cdlemk7u  41743  cdlemk11u  41744  cdlemk33N  41782  cdlemkid2  41797  cdlemkfid3N  41798  cdlemk11ta  41802  cdlemk11tc  41818  cdlemk45  41820  cdlemk46  41821  cdlemk47  41822  cdlemk52  41827  cdlemk53a  41828  cdlemk54  41831  cdlemk55a  41832  cdleml1N  41849  cdleml3N  41851  cdlemn7  42076  cdlemn8  42077  cdlemn10  42079  dihordlem7  42087  dihordlem7b  42088  dihord1  42091  dihord10  42096  dihord11c  42097  dihord2  42100  hlhilphllem  42832  fmuldfeq  46413  seposep  49852  iscnrm3rlem8  49873  iscnrm3llem2  49876