Theorem simp32 1217

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp132  1316  simp232  1325  simp332  1334  eqfunresadj  7304  smogt  8297  axdc3lem4  10366  bitsfzo  16395  frlmphl  21756  mdetunilem4  22598  mdetuni0  22604  mdetmul  22606  decpmatmullem  22754  logfacbnd3  27204  logexprlim  27206  log2sumbnd  27525  nosupfv  27688  nosupres  27689  noinffv  27703  noinfres  27704  ax5seg  29025  numclwwlk1lem2foa  30442  iocinioc2  32871  totprob  34611  cgrtr  36220  cgrtr3  36222  ofscom  36235  cgrextend  36236  segconeq  36238  ifscgr  36272  colinearxfr  36303  brofs2  36305  brifs2  36306  fscgr  36308  btwnconn1lem2  36316  btwnconn1lem9  36323  btwnconn1lem10  36324  btwnconn1lem11  36325  btwnconn1lem12  36326  brsegle2  36337  seglecgr12im  36338  seglecgr12  36339  segletr  36342  outsideofeq  36358  ivthALT  36563  lshpkrlem5  39606  lshpkrlem6  39607  atbtwnexOLDN  39939  atbtwnex  39940  4noncolr3  39945  3dimlem3a  39952  3dim1  39959  3dim2  39960  1cvrat  39968  2atjlej  39971  hlatexch4  39973  ps-2b  39974  2atm  40019  ps-2c  40020  2atmat  40053  4atlem10  40098  4atlem11b  40100  4atlem11  40101  4at  40105  4at2  40106  2lplnja  40111  2lplnj  40112  dalemswapyz  40148  dalem-ddly  40178  cdlemb  40286  paddasslem5  40316  pmodlem1  40338  dalawlem1  40363  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem15  40377  osumcllem5N  40452  osumcllem6N  40453  lhpexle3lem  40503  lhpmcvr4N  40518  lhpmcvr6N  40520  4atexlemex6  40566  4atex2  40569  4atex2-0bOLDN  40571  4atex2-0cOLDN  40572  ltrn11at  40639  trlval3  40679  cdlemd3  40692  cdleme7aa  40734  cdleme7b  40736  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme7  40741  cdleme16aN  40751  cdleme11dN  40754  cdleme11e  40755  cdleme11l  40761  cdleme11  40762  cdleme12  40763  cdleme14  40765  cdleme15a  40766  cdleme15c  40768  cdleme16c  40772  cdleme16d  40773  cdleme16e  40774  cdleme16f  40775  cdleme17c  40780  cdleme18c  40785  cdlemeda  40790  cdlemednpq  40791  cdleme19a  40795  cdleme19c  40797  cdleme20aN  40801  cdleme20bN  40802  cdleme20l1  40812  cdleme20l2  40813  cdleme22aa  40831  cdleme22a  40832  cdleme22g  40840  cdleme23b  40842  cdleme23c  40843  cdleme26fALTN  40854  cdleme26f  40855  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme28b  40863  cdleme32b  40934  cdleme32c  40935  cdleme32e  40937  cdleme35h  40948  cdleme35sn2aw  40950  cdleme38m  40955  cdleme40n  40960  cdleme41sn3aw  40966  cdleme41sn4aw  40967  cdlemeg46gfre  41024  cdlemf1  41053  cdlemg1cex  41080  cdlemg2ce  41084  cdlemg4d  41105  cdlemg4  41109  cdlemg7fvN  41116  cdlemg8b  41120  cdlemg8c  41121  cdlemg9a  41124  cdlemg11aq  41130  cdlemg10a  41132  cdlemg12a  41135  cdlemg12b  41136  cdlemg12d  41138  cdlemg12g  41141  cdlemg12  41142  cdlemg13a  41143  cdlemg13  41144  cdlemg14f  41145  cdlemg14g  41146  cdlemg17b  41154  cdlemg17dN  41155  cdlemg17e  41157  cdlemg17pq  41164  cdlemg17iqN  41166  cdlemg18c  41172  cdlemg18d  41173  cdlemg19a  41175  cdlemg19  41176  cdlemg21  41178  cdlemg27a  41184  cdlemg28a  41185  cdlemg31b0N  41186  cdlemg27b  41188  cdlemg31c  41191  cdlemg33b0  41193  cdlemg28  41196  cdlemg33a  41198  cdlemg33  41203  cdlemg35  41205  cdlemg36  41206  cdlemg44a  41223  cdlemg46  41227  cdlemh2  41308  cdlemh  41309  cdlemj1  41313  cdlemk5  41328  cdlemk6  41329  cdlemki  41333  cdlemksv2  41339  cdlemk7  41340  cdlemk11  41341  cdlemkole  41345  cdlemk14  41346  cdlemk16  41349  cdlemk1u  41351  cdlemk18  41360  cdlemk19  41361  cdlemk7u  41362  cdlemk11u  41363  cdlemk33N  41401  cdlemkid2  41416  cdlemkfid3N  41417  cdlemk11ta  41421  cdlemk11tc  41437  cdlemk45  41439  cdlemk46  41440  cdlemk47  41441  cdlemk52  41446  cdlemk53a  41447  cdlemk54  41450  cdlemk55a  41451  cdleml1N  41468  cdleml3N  41470  cdlemn7  41695  cdlemn8  41696  cdlemn10  41698  dihordlem7  41706  dihordlem7b  41707  dihord1  41710  dihord10  41715  dihord11c  41716  dihord2  41719  hlhilphllem  42451  fmuldfeq  46028  seposep  49416  iscnrm3rlem8  49437  iscnrm3llem2  49440