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  7352  smogt  8379  axdc3lem4  10465  bitsfzo  16452  frlmphl  21739  mdetunilem4  22551  mdetuni0  22557  mdetmul  22559  decpmatmullem  22707  logfacbnd3  27184  logexprlim  27186  log2sumbnd  27505  nosupfv  27668  nosupres  27669  noinffv  27683  noinfres  27684  ax5seg  28863  numclwwlk1lem2foa  30281  iocinioc2  32702  totprob  34405  cgrtr  35956  cgrtr3  35958  ofscom  35971  cgrextend  35972  segconeq  35974  ifscgr  36008  colinearxfr  36039  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem2  36052  btwnconn1lem9  36059  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem12  36062  brsegle2  36073  seglecgr12im  36074  seglecgr12  36075  segletr  36078  outsideofeq  36094  ivthALT  36299  lshpkrlem5  39078  lshpkrlem6  39079  atbtwnexOLDN  39412  atbtwnex  39413  4noncolr3  39418  3dimlem3a  39425  3dim1  39432  3dim2  39433  1cvrat  39441  2atjlej  39444  hlatexch4  39446  ps-2b  39447  2atm  39492  ps-2c  39493  2atmat  39526  4atlem10  39571  4atlem11b  39573  4atlem11  39574  4at  39578  4at2  39579  2lplnja  39584  2lplnj  39585  dalemswapyz  39621  dalem-ddly  39651  cdlemb  39759  paddasslem5  39789  pmodlem1  39811  dalawlem1  39836  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem15  39850  osumcllem5N  39925  osumcllem6N  39926  lhpexle3lem  39976  lhpmcvr4N  39991  lhpmcvr6N  39993  4atexlemex6  40039  4atex2  40042  4atex2-0bOLDN  40044  4atex2-0cOLDN  40045  ltrn11at  40112  trlval3  40152  cdlemd3  40165  cdleme7aa  40207  cdleme7b  40209  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme16aN  40224  cdleme11dN  40227  cdleme11e  40228  cdleme11l  40234  cdleme11  40235  cdleme12  40236  cdleme14  40238  cdleme15a  40239  cdleme15c  40241  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme17c  40253  cdleme18c  40258  cdlemeda  40263  cdlemednpq  40264  cdleme19a  40268  cdleme19c  40270  cdleme20aN  40274  cdleme20bN  40275  cdleme20l1  40285  cdleme20l2  40286  cdleme22aa  40304  cdleme22a  40305  cdleme22g  40313  cdleme23b  40315  cdleme23c  40316  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme28b  40336  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme35h  40421  cdleme35sn2aw  40423  cdleme38m  40428  cdleme40n  40433  cdleme41sn3aw  40439  cdleme41sn4aw  40440  cdlemeg46gfre  40497  cdlemf1  40526  cdlemg1cex  40553  cdlemg2ce  40557  cdlemg4d  40578  cdlemg4  40582  cdlemg7fvN  40589  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg11aq  40603  cdlemg10a  40605  cdlemg12a  40608  cdlemg12b  40609  cdlemg12d  40611  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg14f  40618  cdlemg14g  40619  cdlemg17b  40627  cdlemg17dN  40628  cdlemg17e  40630  cdlemg17pq  40637  cdlemg17iqN  40639  cdlemg18c  40645  cdlemg18d  40646  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg28a  40658  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg28  40669  cdlemg33a  40671  cdlemg33  40676  cdlemg35  40678  cdlemg36  40679  cdlemg44a  40696  cdlemg46  40700  cdlemh2  40781  cdlemh  40782  cdlemj1  40786  cdlemk5  40801  cdlemk6  40802  cdlemki  40806  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemkole  40818  cdlemk14  40819  cdlemk16  40822  cdlemk1u  40824  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk11u  40836  cdlemk33N  40874  cdlemkid2  40889  cdlemkfid3N  40890  cdlemk11ta  40894  cdlemk11tc  40910  cdlemk45  40912  cdlemk46  40913  cdlemk47  40914  cdlemk52  40919  cdlemk53a  40920  cdlemk54  40923  cdlemk55a  40924  cdleml1N  40941  cdleml3N  40943  cdlemn7  41168  cdlemn8  41169  cdlemn10  41171  dihordlem7  41179  dihordlem7b  41180  dihord1  41183  dihord10  41188  dihord11c  41189  dihord2  41192  hlhilphllem  41924  fmuldfeq  45560  seposep  48848  iscnrm3rlem8  48869  iscnrm3llem2  48872