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  7289  smogt  8282  axdc3lem4  10339  bitsfzo  16341  frlmphl  21713  mdetunilem4  22525  mdetuni0  22531  mdetmul  22533  decpmatmullem  22681  logfacbnd3  27156  logexprlim  27158  log2sumbnd  27477  nosupfv  27640  nosupres  27641  noinffv  27655  noinfres  27656  ax5seg  28911  numclwwlk1lem2foa  30326  iocinioc2  32754  totprob  34432  cgrtr  36026  cgrtr3  36028  ofscom  36041  cgrextend  36042  segconeq  36044  ifscgr  36078  colinearxfr  36109  brofs2  36111  brifs2  36112  fscgr  36114  btwnconn1lem2  36122  btwnconn1lem9  36129  btwnconn1lem10  36130  btwnconn1lem11  36131  btwnconn1lem12  36132  brsegle2  36143  seglecgr12im  36144  seglecgr12  36145  segletr  36148  outsideofeq  36164  ivthALT  36369  lshpkrlem5  39153  lshpkrlem6  39154  atbtwnexOLDN  39486  atbtwnex  39487  4noncolr3  39492  3dimlem3a  39499  3dim1  39506  3dim2  39507  1cvrat  39515  2atjlej  39518  hlatexch4  39520  ps-2b  39521  2atm  39566  ps-2c  39567  2atmat  39600  4atlem10  39645  4atlem11b  39647  4atlem11  39648  4at  39652  4at2  39653  2lplnja  39658  2lplnj  39659  dalemswapyz  39695  dalem-ddly  39725  cdlemb  39833  paddasslem5  39863  pmodlem1  39885  dalawlem1  39910  dalawlem3  39912  dalawlem4  39913  dalawlem5  39914  dalawlem6  39915  dalawlem7  39916  dalawlem8  39917  dalawlem9  39918  dalawlem11  39920  dalawlem12  39921  dalawlem15  39924  osumcllem5N  39999  osumcllem6N  40000  lhpexle3lem  40050  lhpmcvr4N  40065  lhpmcvr6N  40067  4atexlemex6  40113  4atex2  40116  4atex2-0bOLDN  40118  4atex2-0cOLDN  40119  ltrn11at  40186  trlval3  40226  cdlemd3  40239  cdleme7aa  40281  cdleme7b  40283  cdleme7c  40284  cdleme7d  40285  cdleme7e  40286  cdleme7ga  40287  cdleme7  40288  cdleme16aN  40298  cdleme11dN  40301  cdleme11e  40302  cdleme11l  40308  cdleme11  40309  cdleme12  40310  cdleme14  40312  cdleme15a  40313  cdleme15c  40315  cdleme16c  40319  cdleme16d  40320  cdleme16e  40321  cdleme16f  40322  cdleme17c  40327  cdleme18c  40332  cdlemeda  40337  cdlemednpq  40338  cdleme19a  40342  cdleme19c  40344  cdleme20aN  40348  cdleme20bN  40349  cdleme20l1  40359  cdleme20l2  40360  cdleme22aa  40378  cdleme22a  40379  cdleme22g  40387  cdleme23b  40389  cdleme23c  40390  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme28b  40410  cdleme32b  40481  cdleme32c  40482  cdleme32e  40484  cdleme35h  40495  cdleme35sn2aw  40497  cdleme38m  40502  cdleme40n  40507  cdleme41sn3aw  40513  cdleme41sn4aw  40514  cdlemeg46gfre  40571  cdlemf1  40600  cdlemg1cex  40627  cdlemg2ce  40631  cdlemg4d  40652  cdlemg4  40656  cdlemg7fvN  40663  cdlemg8b  40667  cdlemg8c  40668  cdlemg9a  40671  cdlemg11aq  40677  cdlemg10a  40679  cdlemg12a  40682  cdlemg12b  40683  cdlemg12d  40685  cdlemg12g  40688  cdlemg12  40689  cdlemg13a  40690  cdlemg13  40691  cdlemg14f  40692  cdlemg14g  40693  cdlemg17b  40701  cdlemg17dN  40702  cdlemg17e  40704  cdlemg17pq  40711  cdlemg17iqN  40713  cdlemg18c  40719  cdlemg18d  40720  cdlemg19a  40722  cdlemg19  40723  cdlemg21  40725  cdlemg27a  40731  cdlemg28a  40732  cdlemg31b0N  40733  cdlemg27b  40735  cdlemg31c  40738  cdlemg33b0  40740  cdlemg28  40743  cdlemg33a  40745  cdlemg33  40750  cdlemg35  40752  cdlemg36  40753  cdlemg44a  40770  cdlemg46  40774  cdlemh2  40855  cdlemh  40856  cdlemj1  40860  cdlemk5  40875  cdlemk6  40876  cdlemki  40880  cdlemksv2  40886  cdlemk7  40887  cdlemk11  40888  cdlemkole  40892  cdlemk14  40893  cdlemk16  40896  cdlemk1u  40898  cdlemk18  40907  cdlemk19  40908  cdlemk7u  40909  cdlemk11u  40910  cdlemk33N  40948  cdlemkid2  40963  cdlemkfid3N  40964  cdlemk11ta  40968  cdlemk11tc  40984  cdlemk45  40986  cdlemk46  40987  cdlemk47  40988  cdlemk52  40993  cdlemk53a  40994  cdlemk54  40997  cdlemk55a  40998  cdleml1N  41015  cdleml3N  41017  cdlemn7  41242  cdlemn8  41243  cdlemn10  41245  dihordlem7  41253  dihordlem7b  41254  dihord1  41257  dihord10  41262  dihord11c  41263  dihord2  41266  hlhilphllem  41998  fmuldfeq  45623  seposep  48957  iscnrm3rlem8  48978  iscnrm3llem2  48981