Theorem simp33 1230

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp33	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1156	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp133  1329  simp233  1338  simp333  1347  eqfunresadj  7358  smogt  8350  bitsfzo  16488  frlmphl  21931  mdetunilem4  22772  mdetuni0  22778  mdetmul  22780  decpmatmullem  22928  logexprlim  27389  noinfres  27886  ax5seg  29288  iocinioc2  33124  bnj966  35332  cgrtr  36484  cgrtr3  36486  ofscom  36499  segconeq  36502  btwnxfr  36548  colinearxfr  36567  fscgr  36572  btwnconn1lem1  36579  btwnconn1lem2  36580  btwnconn1lem5  36583  btwnconn1lem6  36584  btwnconn1lem8  36586  btwnconn1lem9  36587  btwnconn1lem10  36588  btwnconn1lem11  36589  btwnconn1lem12  36590  brsegle2  36601  seglecgr12im  36602  seglecgr12  36603  segletr  36606  outsideofeq  36622  lshpkrlem5  39888  lshpkrlem6  39889  atbtwnexOLDN  40221  atbtwnex  40222  4noncolr3  40227  3dimlem3a  40234  3dimlem4a  40237  3dim1  40241  3dim2  40242  1cvrat  40250  2atjlej  40253  hlatexch4  40255  ps-2b  40256  2atm  40301  ps-2c  40302  lvolex3N  40312  2atmat  40335  lvolnlelpln  40359  4atlem10  40380  4atlem11b  40382  4atlem11  40383  4at  40387  4at2  40388  2lplnja  40393  2lplnj  40394  dalemclccjdd  40462  paddasslem5  40598  paddasslem15  40608  pmodlem1  40620  dalawlem1  40645  dalawlem3  40647  dalawlem4  40648  dalawlem5  40649  dalawlem6  40650  dalawlem7  40651  dalawlem8  40652  dalawlem9  40653  dalawlem11  40655  dalawlem12  40656  dalawlem15  40659  osumcllem5N  40734  osumcllem6N  40735  lhpexle3lem  40785  lhpmcvr4N  40800  lhpmcvr6N  40802  4atexlemex6  40848  4atex2  40851  4atex2-0bOLDN  40853  4atex3  40855  ltrn11at  40921  cdlemd3  40974  cdleme7aa  41016  cdleme7b  41018  cdleme7c  41019  cdleme7d  41020  cdleme7ga  41022  cdleme16aN  41033  cdleme11dN  41036  cdleme11e  41037  cdleme11l  41043  cdleme11  41044  cdleme12  41045  cdleme14  41047  cdleme15c  41050  cdleme16b  41053  cdleme16d  41055  cdleme17b  41061  cdleme17c  41062  cdleme18c  41067  cdleme18d  41069  cdlemeda  41072  cdlemednpq  41073  cdleme19a  41077  cdleme19c  41079  cdleme20aN  41083  cdleme20bN  41084  cdleme20d  41086  cdleme20f  41088  cdleme20g  41089  cdleme20j  41092  cdleme20l1  41094  cdleme21f  41106  cdleme22aa  41113  cdleme22a  41114  cdleme22cN  41116  cdleme22e  41118  cdleme22f2  41121  cdleme22g  41122  cdleme23b  41124  cdleme23c  41125  cdleme26e  41133  cdleme26fALTN  41136  cdleme26f  41137  cdleme26f2ALTN  41138  cdleme26f2  41139  cdleme28a  41144  cdleme28b  41145  cdleme32b  41216  cdleme32c  41217  cdleme32e  41219  cdleme35h2  41231  cdleme38m  41237  cdleme41sn4aw  41249  cdlemf1  41335  cdlemg1cex  41362  cdlemg2ce  41366  cdlemg4d  41387  cdlemg4f  41389  cdlemg7fvN  41398  cdlemg8a  41401  cdlemg8b  41402  cdlemg8c  41403  cdlemg9a  41406  cdlemg11a  41411  cdlemg11aq  41412  cdlemg10a  41414  cdlemg11b  41416  cdlemg12a  41417  cdlemg12b  41418  cdlemg12d  41420  cdlemg12e  41421  cdlemg12f  41422  cdlemg12g  41423  cdlemg12  41424  cdlemg13a  41425  cdlemg13  41426  cdlemg14f  41427  cdlemg14g  41428  cdlemg17b  41436  cdlemg17dN  41437  cdlemg17e  41439  cdlemg17h  41442  cdlemg17pq  41446  cdlemg17iqN  41448  cdlemg18b  41453  cdlemg18c  41454  cdlemg18d  41455  cdlemg18  41456  cdlemg19  41458  cdlemg21  41460  cdlemg27a  41466  cdlemg31b0N  41468  cdlemg27b  41470  cdlemg33b0  41475  cdlemg33c0  41476  cdlemg28  41478  cdlemg33a  41480  cdlemg35  41487  cdlemg42  41503  cdlemg44a  41505  cdlemg47  41510  cdlemh2  41590  cdlemh  41591  cdlemj1  41595  cdlemk3  41607  cdlemk5  41610  cdlemki  41615  cdlemksv2  41621  cdlemk7  41622  cdlemk11  41623  cdlemk12  41624  cdlemkole  41627  cdlemk14  41628  cdlemk15  41629  cdlemk16a  41630  cdlemk16  41631  cdlemkj  41637  cdlemkuv2  41641  cdlemk18  41642  cdlemk19  41643  cdlemk7u  41644  cdlemk12u  41646  cdlemkoatnle-2N  41649  cdlemk13-2N  41650  cdlemkole-2N  41651  cdlemk14-2N  41652  cdlemk15-2N  41653  cdlemk16-2N  41654  cdlemk17-2N  41655  cdlemk18-2N  41660  cdlemk19-2N  41661  cdlemk7u-2N  41662  cdlemk11u-2N  41663  cdlemk12u-2N  41664  cdlemk21-2N  41665  cdlemk20-2N  41666  cdlemk22  41667  cdlemk30  41668  cdlemk31  41670  cdlemk32  41671  cdlemk24-3  41677  cdlemkid2  41698  cdlemkfid3N  41699  cdlemk45  41721  cdlemk46  41722  cdlemk47  41723  cdlemk52  41728  cdlemk53a  41729  cdleml1N  41750  cdleml3N  41752  cdlemn7  41977  cdlemn10  41980  dihordlem7  41988  dihord1  41992  dihord2a  41993  dihord10  41997  dihord11c  41998  dihord2pre2  42000  hlhilphllem  42733  fmuldfeq  46299  usgrgrtrirex  48715  grlimprclnbgredg  48762  seposep  49704  iscnrm3rlem8  49725  iscnrm3llem2  49728