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  7308  smogt  8300  axdc3lem4  10366  bitsfzo  16395  frlmphl  21771  mdetunilem4  22590  mdetuni0  22596  mdetmul  22598  decpmatmullem  22746  logfacbnd3  27200  logexprlim  27202  log2sumbnd  27521  nosupfv  27684  nosupres  27685  noinffv  27699  noinfres  27700  ax5seg  29021  numclwwlk1lem2foa  30439  iocinioc2  32867  totprob  34587  cgrtr  36190  cgrtr3  36192  ofscom  36205  cgrextend  36206  segconeq  36208  ifscgr  36242  colinearxfr  36273  brofs2  36275  brifs2  36276  fscgr  36278  btwnconn1lem2  36286  btwnconn1lem9  36293  btwnconn1lem10  36294  btwnconn1lem11  36295  btwnconn1lem12  36296  brsegle2  36307  seglecgr12im  36308  seglecgr12  36309  segletr  36312  outsideofeq  36328  ivthALT  36533  lshpkrlem5  39574  lshpkrlem6  39575  atbtwnexOLDN  39907  atbtwnex  39908  4noncolr3  39913  3dimlem3a  39920  3dim1  39927  3dim2  39928  1cvrat  39936  2atjlej  39939  hlatexch4  39941  ps-2b  39942  2atm  39987  ps-2c  39988  2atmat  40021  4atlem10  40066  4atlem11b  40068  4atlem11  40069  4at  40073  4at2  40074  2lplnja  40079  2lplnj  40080  dalemswapyz  40116  dalem-ddly  40146  cdlemb  40254  paddasslem5  40284  pmodlem1  40306  dalawlem1  40331  dalawlem3  40333  dalawlem4  40334  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem9  40339  dalawlem11  40341  dalawlem12  40342  dalawlem15  40345  osumcllem5N  40420  osumcllem6N  40421  lhpexle3lem  40471  lhpmcvr4N  40486  lhpmcvr6N  40488  4atexlemex6  40534  4atex2  40537  4atex2-0bOLDN  40539  4atex2-0cOLDN  40540  ltrn11at  40607  trlval3  40647  cdlemd3  40660  cdleme7aa  40702  cdleme7b  40704  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme16aN  40719  cdleme11dN  40722  cdleme11e  40723  cdleme11l  40729  cdleme11  40730  cdleme12  40731  cdleme14  40733  cdleme15a  40734  cdleme15c  40736  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme17c  40748  cdleme18c  40753  cdlemeda  40758  cdlemednpq  40759  cdleme19a  40763  cdleme19c  40765  cdleme20aN  40769  cdleme20bN  40770  cdleme20l1  40780  cdleme20l2  40781  cdleme22aa  40799  cdleme22a  40800  cdleme22g  40808  cdleme23b  40810  cdleme23c  40811  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme28b  40831  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35h  40916  cdleme35sn2aw  40918  cdleme38m  40923  cdleme40n  40928  cdleme41sn3aw  40934  cdleme41sn4aw  40935  cdlemeg46gfre  40992  cdlemf1  41021  cdlemg1cex  41048  cdlemg2ce  41052  cdlemg4d  41073  cdlemg4  41077  cdlemg7fvN  41084  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg11aq  41098  cdlemg10a  41100  cdlemg12a  41103  cdlemg12b  41104  cdlemg12d  41106  cdlemg12g  41109  cdlemg12  41110  cdlemg13a  41111  cdlemg13  41112  cdlemg14f  41113  cdlemg14g  41114  cdlemg17b  41122  cdlemg17dN  41123  cdlemg17e  41125  cdlemg17pq  41132  cdlemg17iqN  41134  cdlemg18c  41140  cdlemg18d  41141  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg28a  41153  cdlemg31b0N  41154  cdlemg27b  41156  cdlemg31c  41159  cdlemg33b0  41161  cdlemg28  41164  cdlemg33a  41166  cdlemg33  41171  cdlemg35  41173  cdlemg36  41174  cdlemg44a  41191  cdlemg46  41195  cdlemh2  41276  cdlemh  41277  cdlemj1  41281  cdlemk5  41296  cdlemk6  41297  cdlemki  41301  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemkole  41313  cdlemk14  41314  cdlemk16  41317  cdlemk1u  41319  cdlemk18  41328  cdlemk19  41329  cdlemk7u  41330  cdlemk11u  41331  cdlemk33N  41369  cdlemkid2  41384  cdlemkfid3N  41385  cdlemk11ta  41389  cdlemk11tc  41405  cdlemk45  41407  cdlemk46  41408  cdlemk47  41409  cdlemk52  41414  cdlemk53a  41415  cdlemk54  41418  cdlemk55a  41419  cdleml1N  41436  cdleml3N  41438  cdlemn7  41663  cdlemn8  41664  cdlemn10  41666  dihordlem7  41674  dihordlem7b  41675  dihord1  41678  dihord10  41683  dihord11c  41684  dihord2  41687  hlhilphllem  42419  fmuldfeq  46031  seposep  49413  iscnrm3rlem8  49434  iscnrm3llem2  49437