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  7303  smogt  8296  axdc3lem4  10355  bitsfzo  16353  frlmphl  21727  mdetunilem4  22550  mdetuni0  22556  mdetmul  22558  decpmatmullem  22706  logfacbnd3  27181  logexprlim  27183  log2sumbnd  27502  nosupfv  27665  nosupres  27666  noinffv  27680  noinfres  27681  ax5seg  28937  numclwwlk1lem2foa  30355  iocinioc2  32787  totprob  34512  cgrtr  36108  cgrtr3  36110  ofscom  36123  cgrextend  36124  segconeq  36126  ifscgr  36160  colinearxfr  36191  brofs2  36193  brifs2  36194  fscgr  36196  btwnconn1lem2  36204  btwnconn1lem9  36211  btwnconn1lem10  36212  btwnconn1lem11  36213  btwnconn1lem12  36214  brsegle2  36225  seglecgr12im  36226  seglecgr12  36227  segletr  36230  outsideofeq  36246  ivthALT  36451  lshpkrlem5  39286  lshpkrlem6  39287  atbtwnexOLDN  39619  atbtwnex  39620  4noncolr3  39625  3dimlem3a  39632  3dim1  39639  3dim2  39640  1cvrat  39648  2atjlej  39651  hlatexch4  39653  ps-2b  39654  2atm  39699  ps-2c  39700  2atmat  39733  4atlem10  39778  4atlem11b  39780  4atlem11  39781  4at  39785  4at2  39786  2lplnja  39791  2lplnj  39792  dalemswapyz  39828  dalem-ddly  39858  cdlemb  39966  paddasslem5  39996  pmodlem1  40018  dalawlem1  40043  dalawlem3  40045  dalawlem4  40046  dalawlem5  40047  dalawlem6  40048  dalawlem7  40049  dalawlem8  40050  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem15  40057  osumcllem5N  40132  osumcllem6N  40133  lhpexle3lem  40183  lhpmcvr4N  40198  lhpmcvr6N  40200  4atexlemex6  40246  4atex2  40249  4atex2-0bOLDN  40251  4atex2-0cOLDN  40252  ltrn11at  40319  trlval3  40359  cdlemd3  40372  cdleme7aa  40414  cdleme7b  40416  cdleme7c  40417  cdleme7d  40418  cdleme7e  40419  cdleme7ga  40420  cdleme7  40421  cdleme16aN  40431  cdleme11dN  40434  cdleme11e  40435  cdleme11l  40441  cdleme11  40442  cdleme12  40443  cdleme14  40445  cdleme15a  40446  cdleme15c  40448  cdleme16c  40452  cdleme16d  40453  cdleme16e  40454  cdleme16f  40455  cdleme17c  40460  cdleme18c  40465  cdlemeda  40470  cdlemednpq  40471  cdleme19a  40475  cdleme19c  40477  cdleme20aN  40481  cdleme20bN  40482  cdleme20l1  40492  cdleme20l2  40493  cdleme22aa  40511  cdleme22a  40512  cdleme22g  40520  cdleme23b  40522  cdleme23c  40523  cdleme26fALTN  40534  cdleme26f  40535  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme28b  40543  cdleme32b  40614  cdleme32c  40615  cdleme32e  40617  cdleme35h  40628  cdleme35sn2aw  40630  cdleme38m  40635  cdleme40n  40640  cdleme41sn3aw  40646  cdleme41sn4aw  40647  cdlemeg46gfre  40704  cdlemf1  40733  cdlemg1cex  40760  cdlemg2ce  40764  cdlemg4d  40785  cdlemg4  40789  cdlemg7fvN  40796  cdlemg8b  40800  cdlemg8c  40801  cdlemg9a  40804  cdlemg11aq  40810  cdlemg10a  40812  cdlemg12a  40815  cdlemg12b  40816  cdlemg12d  40818  cdlemg12g  40821  cdlemg12  40822  cdlemg13a  40823  cdlemg13  40824  cdlemg14f  40825  cdlemg14g  40826  cdlemg17b  40834  cdlemg17dN  40835  cdlemg17e  40837  cdlemg17pq  40844  cdlemg17iqN  40846  cdlemg18c  40852  cdlemg18d  40853  cdlemg19a  40855  cdlemg19  40856  cdlemg21  40858  cdlemg27a  40864  cdlemg28a  40865  cdlemg31b0N  40866  cdlemg27b  40868  cdlemg31c  40871  cdlemg33b0  40873  cdlemg28  40876  cdlemg33a  40878  cdlemg33  40883  cdlemg35  40885  cdlemg36  40886  cdlemg44a  40903  cdlemg46  40907  cdlemh2  40988  cdlemh  40989  cdlemj1  40993  cdlemk5  41008  cdlemk6  41009  cdlemki  41013  cdlemksv2  41019  cdlemk7  41020  cdlemk11  41021  cdlemkole  41025  cdlemk14  41026  cdlemk16  41029  cdlemk1u  41031  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk11u  41043  cdlemk33N  41081  cdlemkid2  41096  cdlemkfid3N  41097  cdlemk11ta  41101  cdlemk11tc  41117  cdlemk45  41119  cdlemk46  41120  cdlemk47  41121  cdlemk52  41126  cdlemk53a  41127  cdlemk54  41130  cdlemk55a  41131  cdleml1N  41148  cdleml3N  41150  cdlemn7  41375  cdlemn8  41376  cdlemn10  41378  dihordlem7  41386  dihordlem7b  41387  dihord1  41390  dihord10  41395  dihord11c  41396  dihord2  41399  hlhilphllem  42131  fmuldfeq  45745  seposep  49087  iscnrm3rlem8  49108  iscnrm3llem2  49111