Theorem simp32 1210

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 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  simp132  1309  simp232  1318  simp332  1327  smogt  8229  axdc3lem4  10255  bitsfzo  16187  frlmphl  21033  mdetunilem4  21809  mdetuni0  21815  mdetmul  21817  decpmatmullem  21965  logfacbnd3  26416  logexprlim  26418  log2sumbnd  26737  ax5seg  27351  numclwwlk1lem2foa  28763  iocinioc2  31145  totprob  32439  eqfunresadj  33780  nosupfv  33954  nosupres  33955  noinffv  33969  noinfres  33970  cgrtr  34339  cgrtr3  34341  ofscom  34354  cgrextend  34355  segconeq  34357  ifscgr  34391  colinearxfr  34422  brofs2  34424  brifs2  34425  fscgr  34427  btwnconn1lem2  34435  btwnconn1lem9  34442  btwnconn1lem10  34443  btwnconn1lem11  34444  btwnconn1lem12  34445  brsegle2  34456  seglecgr12im  34457  seglecgr12  34458  segletr  34461  outsideofeq  34477  ivthALT  34569  lshpkrlem5  37170  lshpkrlem6  37171  atbtwnexOLDN  37503  atbtwnex  37504  4noncolr3  37509  3dimlem3a  37516  3dim1  37523  3dim2  37524  1cvrat  37532  2atjlej  37535  hlatexch4  37537  ps-2b  37538  2atm  37583  ps-2c  37584  2atmat  37617  4atlem10  37662  4atlem11b  37664  4atlem11  37665  4at  37669  4at2  37670  2lplnja  37675  2lplnj  37676  dalemswapyz  37712  dalem-ddly  37742  cdlemb  37850  paddasslem5  37880  pmodlem1  37902  dalawlem1  37927  dalawlem3  37929  dalawlem4  37930  dalawlem5  37931  dalawlem6  37932  dalawlem7  37933  dalawlem8  37934  dalawlem9  37935  dalawlem11  37937  dalawlem12  37938  dalawlem15  37941  osumcllem5N  38016  osumcllem6N  38017  lhpexle3lem  38067  lhpmcvr4N  38082  lhpmcvr6N  38084  4atexlemex6  38130  4atex2  38133  4atex2-0bOLDN  38135  4atex2-0cOLDN  38136  ltrn11at  38203  trlval3  38243  cdlemd3  38256  cdleme7aa  38298  cdleme7b  38300  cdleme7c  38301  cdleme7d  38302  cdleme7e  38303  cdleme7ga  38304  cdleme7  38305  cdleme16aN  38315  cdleme11dN  38318  cdleme11e  38319  cdleme11l  38325  cdleme11  38326  cdleme12  38327  cdleme14  38329  cdleme15a  38330  cdleme15c  38332  cdleme16c  38336  cdleme16d  38337  cdleme16e  38338  cdleme16f  38339  cdleme17c  38344  cdleme18c  38349  cdlemeda  38354  cdlemednpq  38355  cdleme19a  38359  cdleme19c  38361  cdleme20aN  38365  cdleme20bN  38366  cdleme20l1  38376  cdleme20l2  38377  cdleme22aa  38395  cdleme22a  38396  cdleme22g  38404  cdleme23b  38406  cdleme23c  38407  cdleme26fALTN  38418  cdleme26f  38419  cdleme26f2ALTN  38420  cdleme26f2  38421  cdleme28b  38427  cdleme32b  38498  cdleme32c  38499  cdleme32e  38501  cdleme35h  38512  cdleme35sn2aw  38514  cdleme38m  38519  cdleme40n  38524  cdleme41sn3aw  38530  cdleme41sn4aw  38531  cdlemeg46gfre  38588  cdlemf1  38617  cdlemg1cex  38644  cdlemg2ce  38648  cdlemg4d  38669  cdlemg4  38673  cdlemg7fvN  38680  cdlemg8b  38684  cdlemg8c  38685  cdlemg9a  38688  cdlemg11aq  38694  cdlemg10a  38696  cdlemg12a  38699  cdlemg12b  38700  cdlemg12d  38702  cdlemg12g  38705  cdlemg12  38706  cdlemg13a  38707  cdlemg13  38708  cdlemg14f  38709  cdlemg14g  38710  cdlemg17b  38718  cdlemg17dN  38719  cdlemg17e  38721  cdlemg17pq  38728  cdlemg17iqN  38730  cdlemg18c  38736  cdlemg18d  38737  cdlemg19a  38739  cdlemg19  38740  cdlemg21  38742  cdlemg27a  38748  cdlemg28a  38749  cdlemg31b0N  38750  cdlemg27b  38752  cdlemg31c  38755  cdlemg33b0  38757  cdlemg28  38760  cdlemg33a  38762  cdlemg33  38767  cdlemg35  38769  cdlemg36  38770  cdlemg44a  38787  cdlemg46  38791  cdlemh2  38872  cdlemh  38873  cdlemj1  38877  cdlemk5  38892  cdlemk6  38893  cdlemki  38897  cdlemksv2  38903  cdlemk7  38904  cdlemk11  38905  cdlemkole  38909  cdlemk14  38910  cdlemk16  38913  cdlemk1u  38915  cdlemk18  38924  cdlemk19  38925  cdlemk7u  38926  cdlemk11u  38927  cdlemk33N  38965  cdlemkid2  38980  cdlemkfid3N  38981  cdlemk11ta  38985  cdlemk11tc  39001  cdlemk45  39003  cdlemk46  39004  cdlemk47  39005  cdlemk52  39010  cdlemk53a  39011  cdlemk54  39014  cdlemk55a  39015  cdleml1N  39032  cdleml3N  39034  cdlemn7  39259  cdlemn8  39260  cdlemn10  39262  dihordlem7  39270  dihordlem7b  39271  dihord1  39274  dihord10  39279  dihord11c  39280  dihord2  39283  hlhilphllem  40019  fmuldfeq  43173  seposep  46277  iscnrm3rlem8  46299  iscnrm3llem2  46302