Theorem simp32 1212

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 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp132  1311  simp232  1320  simp332  1329  eqfunresadj  7316  smogt  8309  axdc3lem4  10375  bitsfzo  16374  frlmphl  21748  mdetunilem4  22571  mdetuni0  22577  mdetmul  22579  decpmatmullem  22727  logfacbnd3  27202  logexprlim  27204  log2sumbnd  27523  nosupfv  27686  nosupres  27687  noinffv  27701  noinfres  27702  ax5seg  29023  numclwwlk1lem2foa  30441  iocinioc2  32869  totprob  34604  cgrtr  36205  cgrtr3  36207  ofscom  36220  cgrextend  36221  segconeq  36223  ifscgr  36257  colinearxfr  36288  brofs2  36290  brifs2  36291  fscgr  36293  btwnconn1lem2  36301  btwnconn1lem9  36308  btwnconn1lem10  36309  btwnconn1lem11  36310  btwnconn1lem12  36311  brsegle2  36322  seglecgr12im  36323  seglecgr12  36324  segletr  36327  outsideofeq  36343  ivthALT  36548  lshpkrlem5  39487  lshpkrlem6  39488  atbtwnexOLDN  39820  atbtwnex  39821  4noncolr3  39826  3dimlem3a  39833  3dim1  39840  3dim2  39841  1cvrat  39849  2atjlej  39852  hlatexch4  39854  ps-2b  39855  2atm  39900  ps-2c  39901  2atmat  39934  4atlem10  39979  4atlem11b  39981  4atlem11  39982  4at  39986  4at2  39987  2lplnja  39992  2lplnj  39993  dalemswapyz  40029  dalem-ddly  40059  cdlemb  40167  paddasslem5  40197  pmodlem1  40219  dalawlem1  40244  dalawlem3  40246  dalawlem4  40247  dalawlem5  40248  dalawlem6  40249  dalawlem7  40250  dalawlem8  40251  dalawlem9  40252  dalawlem11  40254  dalawlem12  40255  dalawlem15  40258  osumcllem5N  40333  osumcllem6N  40334  lhpexle3lem  40384  lhpmcvr4N  40399  lhpmcvr6N  40401  4atexlemex6  40447  4atex2  40450  4atex2-0bOLDN  40452  4atex2-0cOLDN  40453  ltrn11at  40520  trlval3  40560  cdlemd3  40573  cdleme7aa  40615  cdleme7b  40617  cdleme7c  40618  cdleme7d  40619  cdleme7e  40620  cdleme7ga  40621  cdleme7  40622  cdleme16aN  40632  cdleme11dN  40635  cdleme11e  40636  cdleme11l  40642  cdleme11  40643  cdleme12  40644  cdleme14  40646  cdleme15a  40647  cdleme15c  40649  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme16f  40656  cdleme17c  40661  cdleme18c  40666  cdlemeda  40671  cdlemednpq  40672  cdleme19a  40676  cdleme19c  40678  cdleme20aN  40682  cdleme20bN  40683  cdleme20l1  40693  cdleme20l2  40694  cdleme22aa  40712  cdleme22a  40713  cdleme22g  40721  cdleme23b  40723  cdleme23c  40724  cdleme26fALTN  40735  cdleme26f  40736  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme28b  40744  cdleme32b  40815  cdleme32c  40816  cdleme32e  40818  cdleme35h  40829  cdleme35sn2aw  40831  cdleme38m  40836  cdleme40n  40841  cdleme41sn3aw  40847  cdleme41sn4aw  40848  cdlemeg46gfre  40905  cdlemf1  40934  cdlemg1cex  40961  cdlemg2ce  40965  cdlemg4d  40986  cdlemg4  40990  cdlemg7fvN  40997  cdlemg8b  41001  cdlemg8c  41002  cdlemg9a  41005  cdlemg11aq  41011  cdlemg10a  41013  cdlemg12a  41016  cdlemg12b  41017  cdlemg12d  41019  cdlemg12g  41022  cdlemg12  41023  cdlemg13a  41024  cdlemg13  41025  cdlemg14f  41026  cdlemg14g  41027  cdlemg17b  41035  cdlemg17dN  41036  cdlemg17e  41038  cdlemg17pq  41045  cdlemg17iqN  41047  cdlemg18c  41053  cdlemg18d  41054  cdlemg19a  41056  cdlemg19  41057  cdlemg21  41059  cdlemg27a  41065  cdlemg28a  41066  cdlemg31b0N  41067  cdlemg27b  41069  cdlemg31c  41072  cdlemg33b0  41074  cdlemg28  41077  cdlemg33a  41079  cdlemg33  41084  cdlemg35  41086  cdlemg36  41087  cdlemg44a  41104  cdlemg46  41108  cdlemh2  41189  cdlemh  41190  cdlemj1  41194  cdlemk5  41209  cdlemk6  41210  cdlemki  41214  cdlemksv2  41220  cdlemk7  41221  cdlemk11  41222  cdlemkole  41226  cdlemk14  41227  cdlemk16  41230  cdlemk1u  41232  cdlemk18  41241  cdlemk19  41242  cdlemk7u  41243  cdlemk11u  41244  cdlemk33N  41282  cdlemkid2  41297  cdlemkfid3N  41298  cdlemk11ta  41302  cdlemk11tc  41318  cdlemk45  41320  cdlemk46  41321  cdlemk47  41322  cdlemk52  41327  cdlemk53a  41328  cdlemk54  41331  cdlemk55a  41332  cdleml1N  41349  cdleml3N  41351  cdlemn7  41576  cdlemn8  41577  cdlemn10  41579  dihordlem7  41587  dihordlem7b  41588  dihord1  41591  dihord10  41596  dihord11c  41597  dihord2  41600  hlhilphllem  42332  fmuldfeq  45940  seposep  49282  iscnrm3rlem8  49303  iscnrm3llem2  49306