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 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1136	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1088

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 400  df-3an 1090

This theorem is referenced by:  simp132  1310  simp232  1319  simp332  1328  smogt  8026  axdc3lem4  9946  bitsfzo  15871  frlmphl  20590  mdetunilem4  21359  mdetuni0  21365  mdetmul  21367  decpmatmullem  21515  logfacbnd3  25951  logexprlim  25953  log2sumbnd  26272  ax5seg  26876  numclwwlk1lem2foa  28283  iocinioc2  30667  totprob  31956  eqfunresadj  33299  nosupfv  33542  nosupres  33543  noinffv  33557  noinfres  33558  cgrtr  33924  cgrtr3  33926  ofscom  33939  cgrextend  33940  segconeq  33942  ifscgr  33976  colinearxfr  34007  brofs2  34009  brifs2  34010  fscgr  34012  btwnconn1lem2  34020  btwnconn1lem9  34027  btwnconn1lem10  34028  btwnconn1lem11  34029  btwnconn1lem12  34030  brsegle2  34041  seglecgr12im  34042  seglecgr12  34043  segletr  34046  outsideofeq  34062  ivthALT  34154  lshpkrlem5  36740  lshpkrlem6  36741  atbtwnexOLDN  37073  atbtwnex  37074  4noncolr3  37079  3dimlem3a  37086  3dim1  37093  3dim2  37094  1cvrat  37102  2atjlej  37105  hlatexch4  37107  ps-2b  37108  2atm  37153  ps-2c  37154  2atmat  37187  4atlem10  37232  4atlem11b  37234  4atlem11  37235  4at  37239  4at2  37240  2lplnja  37245  2lplnj  37246  dalemswapyz  37282  dalem-ddly  37312  cdlemb  37420  paddasslem5  37450  pmodlem1  37472  dalawlem1  37497  dalawlem3  37499  dalawlem4  37500  dalawlem5  37501  dalawlem6  37502  dalawlem7  37503  dalawlem8  37504  dalawlem9  37505  dalawlem11  37507  dalawlem12  37508  dalawlem15  37511  osumcllem5N  37586  osumcllem6N  37587  lhpexle3lem  37637  lhpmcvr4N  37652  lhpmcvr6N  37654  4atexlemex6  37700  4atex2  37703  4atex2-0bOLDN  37705  4atex2-0cOLDN  37706  ltrn11at  37773  trlval3  37813  cdlemd3  37826  cdleme7aa  37868  cdleme7b  37870  cdleme7c  37871  cdleme7d  37872  cdleme7e  37873  cdleme7ga  37874  cdleme7  37875  cdleme16aN  37885  cdleme11dN  37888  cdleme11e  37889  cdleme11l  37895  cdleme11  37896  cdleme12  37897  cdleme14  37899  cdleme15a  37900  cdleme15c  37902  cdleme16c  37906  cdleme16d  37907  cdleme16e  37908  cdleme16f  37909  cdleme17c  37914  cdleme18c  37919  cdlemeda  37924  cdlemednpq  37925  cdleme19a  37929  cdleme19c  37931  cdleme20aN  37935  cdleme20bN  37936  cdleme20l1  37946  cdleme20l2  37947  cdleme22aa  37965  cdleme22a  37966  cdleme22g  37974  cdleme23b  37976  cdleme23c  37977  cdleme26fALTN  37988  cdleme26f  37989  cdleme26f2ALTN  37990  cdleme26f2  37991  cdleme28b  37997  cdleme32b  38068  cdleme32c  38069  cdleme32e  38071  cdleme35h  38082  cdleme35sn2aw  38084  cdleme38m  38089  cdleme40n  38094  cdleme41sn3aw  38100  cdleme41sn4aw  38101  cdlemeg46gfre  38158  cdlemf1  38187  cdlemg1cex  38214  cdlemg2ce  38218  cdlemg4d  38239  cdlemg4  38243  cdlemg7fvN  38250  cdlemg8b  38254  cdlemg8c  38255  cdlemg9a  38258  cdlemg11aq  38264  cdlemg10a  38266  cdlemg12a  38269  cdlemg12b  38270  cdlemg12d  38272  cdlemg12g  38275  cdlemg12  38276  cdlemg13a  38277  cdlemg13  38278  cdlemg14f  38279  cdlemg14g  38280  cdlemg17b  38288  cdlemg17dN  38289  cdlemg17e  38291  cdlemg17pq  38298  cdlemg17iqN  38300  cdlemg18c  38306  cdlemg18d  38307  cdlemg19a  38309  cdlemg19  38310  cdlemg21  38312  cdlemg27a  38318  cdlemg28a  38319  cdlemg31b0N  38320  cdlemg27b  38322  cdlemg31c  38325  cdlemg33b0  38327  cdlemg28  38330  cdlemg33a  38332  cdlemg33  38337  cdlemg35  38339  cdlemg36  38340  cdlemg44a  38357  cdlemg46  38361  cdlemh2  38442  cdlemh  38443  cdlemj1  38447  cdlemk5  38462  cdlemk6  38463  cdlemki  38467  cdlemksv2  38473  cdlemk7  38474  cdlemk11  38475  cdlemkole  38479  cdlemk14  38480  cdlemk16  38483  cdlemk1u  38485  cdlemk18  38494  cdlemk19  38495  cdlemk7u  38496  cdlemk11u  38497  cdlemk33N  38535  cdlemkid2  38550  cdlemkfid3N  38551  cdlemk11ta  38555  cdlemk11tc  38571  cdlemk45  38573  cdlemk46  38574  cdlemk47  38575  cdlemk52  38580  cdlemk53a  38581  cdlemk54  38584  cdlemk55a  38585  cdleml1N  38602  cdleml3N  38604  cdlemn7  38829  cdlemn8  38830  cdlemn10  38832  dihordlem7  38840  dihordlem7b  38841  dihord1  38844  dihord10  38849  dihord11c  38850  dihord2  38853  hlhilphllem  39585  fmuldfeq  42650  seposep  45725  iscnrm3rlem8  45747  iscnrm3llem2  45750