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 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp132  1328  simp232  1337  simp332  1346  eqfunresadj  7360  smogt  8355  axdc3lem4  10438  bitsfzo  16494  frlmphl  21912  mdetunilem4  22753  mdetuni0  22759  mdetmul  22761  decpmatmullem  22909  logfacbnd3  27368  logexprlim  27370  log2sumbnd  27689  nosupfv  27851  nosupres  27852  noinffv  27866  noinfres  27867  ax5seg  29269  numclwwlk1lem2foa  30686  iocinioc2  33105  totprob  34798  cgrtr  36465  cgrtr3  36467  ofscom  36480  cgrextend  36481  segconeq  36483  ifscgr  36517  colinearxfr  36548  brofs2  36550  brifs2  36551  fscgr  36553  btwnconn1lem2  36561  btwnconn1lem9  36568  btwnconn1lem10  36569  btwnconn1lem11  36570  btwnconn1lem12  36571  brsegle2  36582  seglecgr12im  36583  seglecgr12  36584  segletr  36587  outsideofeq  36603  ivthALT  36827  lshpkrlem5  39869  lshpkrlem6  39870  atbtwnexOLDN  40202  atbtwnex  40203  4noncolr3  40208  3dimlem3a  40215  3dim1  40222  3dim2  40223  1cvrat  40231  2atjlej  40234  hlatexch4  40236  ps-2b  40237  2atm  40282  ps-2c  40283  2atmat  40316  4atlem10  40361  4atlem11b  40363  4atlem11  40364  4at  40368  4at2  40369  2lplnja  40374  2lplnj  40375  dalemswapyz  40411  dalem-ddly  40441  cdlemb  40549  paddasslem5  40579  pmodlem1  40601  dalawlem1  40626  dalawlem3  40628  dalawlem4  40629  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem9  40634  dalawlem11  40636  dalawlem12  40637  dalawlem15  40640  osumcllem5N  40715  osumcllem6N  40716  lhpexle3lem  40766  lhpmcvr4N  40781  lhpmcvr6N  40783  4atexlemex6  40829  4atex2  40832  4atex2-0bOLDN  40834  4atex2-0cOLDN  40835  ltrn11at  40902  trlval3  40942  cdlemd3  40955  cdleme7aa  40997  cdleme7b  40999  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme16aN  41014  cdleme11dN  41017  cdleme11e  41018  cdleme11l  41024  cdleme11  41025  cdleme12  41026  cdleme14  41028  cdleme15a  41029  cdleme15c  41031  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme17c  41043  cdleme18c  41048  cdlemeda  41053  cdlemednpq  41054  cdleme19a  41058  cdleme19c  41060  cdleme20aN  41064  cdleme20bN  41065  cdleme20l1  41075  cdleme20l2  41076  cdleme22aa  41094  cdleme22a  41095  cdleme22g  41103  cdleme23b  41105  cdleme23c  41106  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme28b  41126  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme35h  41211  cdleme35sn2aw  41213  cdleme38m  41218  cdleme40n  41223  cdleme41sn3aw  41229  cdleme41sn4aw  41230  cdlemeg46gfre  41287  cdlemf1  41316  cdlemg1cex  41343  cdlemg2ce  41347  cdlemg4d  41368  cdlemg4  41372  cdlemg7fvN  41379  cdlemg8b  41383  cdlemg8c  41384  cdlemg9a  41387  cdlemg11aq  41393  cdlemg10a  41395  cdlemg12a  41398  cdlemg12b  41399  cdlemg12d  41401  cdlemg12g  41404  cdlemg12  41405  cdlemg13a  41406  cdlemg13  41407  cdlemg14f  41408  cdlemg14g  41409  cdlemg17b  41417  cdlemg17dN  41418  cdlemg17e  41420  cdlemg17pq  41427  cdlemg17iqN  41429  cdlemg18c  41435  cdlemg18d  41436  cdlemg19a  41438  cdlemg19  41439  cdlemg21  41441  cdlemg27a  41447  cdlemg28a  41448  cdlemg31b0N  41449  cdlemg27b  41451  cdlemg31c  41454  cdlemg33b0  41456  cdlemg28  41459  cdlemg33a  41461  cdlemg33  41466  cdlemg35  41468  cdlemg36  41469  cdlemg44a  41486  cdlemg46  41490  cdlemh2  41571  cdlemh  41572  cdlemj1  41576  cdlemk5  41591  cdlemk6  41592  cdlemki  41596  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemkole  41608  cdlemk14  41609  cdlemk16  41612  cdlemk1u  41614  cdlemk18  41623  cdlemk19  41624  cdlemk7u  41625  cdlemk11u  41626  cdlemk33N  41664  cdlemkid2  41679  cdlemkfid3N  41680  cdlemk11ta  41684  cdlemk11tc  41700  cdlemk45  41702  cdlemk46  41703  cdlemk47  41704  cdlemk52  41709  cdlemk53a  41710  cdlemk54  41713  cdlemk55a  41714  cdleml1N  41731  cdleml3N  41733  cdlemn7  41958  cdlemn8  41959  cdlemn10  41961  dihordlem7  41969  dihordlem7b  41970  dihord1  41973  dihord10  41978  dihord11c  41979  dihord2  41982  hlhilphllem  42714  fmuldfeq  46282  seposep  49687  iscnrm3rlem8  49708  iscnrm3llem2  49711