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  7368  smogt  8368  axdc3lem4  10524  bitsfzo  16598  frlmphl  22080  mdetunilem4  22923  mdetuni0  22929  mdetmul  22931  decpmatmullem  23082  logfacbnd3  27543  logexprlim  27545  log2sumbnd  27864  nosupfv  28056  nosupres  28057  noinffv  28071  noinfres  28072  ax5seg  29509  numclwwlk1lem2foa  30948  iocinioc2  33364  totprob  35052  cgrtr  36737  cgrtr3  36739  ofscom  36752  cgrextend  36753  segconeq  36755  ifscgr  36789  colinearxfr  36820  brofs2  36822  brifs2  36823  fscgr  36825  btwnconn1lem2  36833  btwnconn1lem9  36840  btwnconn1lem10  36841  btwnconn1lem11  36842  btwnconn1lem12  36843  brsegle2  36854  seglecgr12im  36855  seglecgr12  36856  segletr  36859  outsideofeq  36875  ivthALT  37103  lshpkrlem5  40151  lshpkrlem6  40152  atbtwnexOLDN  40484  atbtwnex  40485  4noncolr3  40490  3dimlem3a  40497  3dim1  40504  3dim2  40505  1cvrat  40513  2atjlej  40516  hlatexch4  40518  ps-2b  40519  2atm  40564  ps-2c  40565  2atmat  40598  4atlem10  40643  4atlem11b  40645  4atlem11  40646  4at  40650  4at2  40651  2lplnja  40656  2lplnj  40657  dalemswapyz  40693  dalem-ddly  40723  cdlemb  40831  paddasslem5  40861  pmodlem1  40883  dalawlem1  40908  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem15  40922  osumcllem5N  40997  osumcllem6N  40998  lhpexle3lem  41048  lhpmcvr4N  41063  lhpmcvr6N  41065  4atexlemex6  41111  4atex2  41114  4atex2-0bOLDN  41116  4atex2-0cOLDN  41117  ltrn11at  41184  trlval3  41224  cdlemd3  41237  cdleme7aa  41279  cdleme7b  41281  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme7ga  41285  cdleme7  41286  cdleme16aN  41296  cdleme11dN  41299  cdleme11e  41300  cdleme11l  41306  cdleme11  41307  cdleme12  41308  cdleme14  41310  cdleme15a  41311  cdleme15c  41313  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme17c  41325  cdleme18c  41330  cdlemeda  41335  cdlemednpq  41336  cdleme19a  41340  cdleme19c  41342  cdleme20aN  41346  cdleme20bN  41347  cdleme20l1  41357  cdleme20l2  41358  cdleme22aa  41376  cdleme22a  41377  cdleme22g  41385  cdleme23b  41387  cdleme23c  41388  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme28b  41408  cdleme32b  41479  cdleme32c  41480  cdleme32e  41482  cdleme35h  41493  cdleme35sn2aw  41495  cdleme38m  41500  cdleme40n  41505  cdleme41sn3aw  41511  cdleme41sn4aw  41512  cdlemeg46gfre  41569  cdlemf1  41598  cdlemg1cex  41625  cdlemg2ce  41629  cdlemg4d  41650  cdlemg4  41654  cdlemg7fvN  41661  cdlemg8b  41665  cdlemg8c  41666  cdlemg9a  41669  cdlemg11aq  41675  cdlemg10a  41677  cdlemg12a  41680  cdlemg12b  41681  cdlemg12d  41683  cdlemg12g  41686  cdlemg12  41687  cdlemg13a  41688  cdlemg13  41689  cdlemg14f  41690  cdlemg14g  41691  cdlemg17b  41699  cdlemg17dN  41700  cdlemg17e  41702  cdlemg17pq  41709  cdlemg17iqN  41711  cdlemg18c  41717  cdlemg18d  41718  cdlemg19a  41720  cdlemg19  41721  cdlemg21  41723  cdlemg27a  41729  cdlemg28a  41730  cdlemg31b0N  41731  cdlemg27b  41733  cdlemg31c  41736  cdlemg33b0  41738  cdlemg28  41741  cdlemg33a  41743  cdlemg33  41748  cdlemg35  41750  cdlemg36  41751  cdlemg44a  41768  cdlemg46  41772  cdlemh2  41853  cdlemh  41854  cdlemj1  41858  cdlemk5  41873  cdlemk6  41874  cdlemki  41878  cdlemksv2  41884  cdlemk7  41885  cdlemk11  41886  cdlemkole  41890  cdlemk14  41891  cdlemk16  41894  cdlemk1u  41896  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk11u  41908  cdlemk33N  41946  cdlemkid2  41961  cdlemkfid3N  41962  cdlemk11ta  41966  cdlemk11tc  41982  cdlemk45  41984  cdlemk46  41985  cdlemk47  41986  cdlemk52  41991  cdlemk53a  41992  cdlemk54  41995  cdlemk55a  41996  cdleml1N  42013  cdleml3N  42015  cdlemn7  42240  cdlemn8  42241  cdlemn10  42243  dihordlem7  42251  dihordlem7b  42252  dihord1  42255  dihord10  42260  dihord11c  42261  dihord2  42264  hlhilphllem  42996  fmuldfeq  46564  seposep  50003  iscnrm3rlem8  50024  iscnrm3llem2  50027