Theorem simp33 1213

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 1139	. 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:  simp133  1312  simp233  1321  simp333  1330  eqfunresadj  7315  smogt  8307  bitsfzo  16404  frlmphl  21761  mdetunilem4  22580  mdetuni0  22586  mdetmul  22588  decpmatmullem  22736  logexprlim  27188  noinfres  27686  ax5seg  29007  iocinioc2  32852  bnj966  35086  cgrtr  36174  cgrtr3  36176  ofscom  36189  segconeq  36192  btwnxfr  36238  colinearxfr  36257  fscgr  36262  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem12  36280  brsegle2  36291  seglecgr12im  36292  seglecgr12  36293  segletr  36296  outsideofeq  36312  lshpkrlem5  39560  lshpkrlem6  39561  atbtwnexOLDN  39893  atbtwnex  39894  4noncolr3  39899  3dimlem3a  39906  3dimlem4a  39909  3dim1  39913  3dim2  39914  1cvrat  39922  2atjlej  39925  hlatexch4  39927  ps-2b  39928  2atm  39973  ps-2c  39974  lvolex3N  39984  2atmat  40007  lvolnlelpln  40031  4atlem10  40052  4atlem11b  40054  4atlem11  40055  4at  40059  4at2  40060  2lplnja  40065  2lplnj  40066  dalemclccjdd  40134  paddasslem5  40270  paddasslem15  40280  pmodlem1  40292  dalawlem1  40317  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  osumcllem5N  40406  osumcllem6N  40407  lhpexle3lem  40457  lhpmcvr4N  40472  lhpmcvr6N  40474  4atexlemex6  40520  4atex2  40523  4atex2-0bOLDN  40525  4atex3  40527  ltrn11at  40593  cdlemd3  40646  cdleme7aa  40688  cdleme7b  40690  cdleme7c  40691  cdleme7d  40692  cdleme7ga  40694  cdleme16aN  40705  cdleme11dN  40708  cdleme11e  40709  cdleme11l  40715  cdleme11  40716  cdleme12  40717  cdleme14  40719  cdleme15c  40722  cdleme16b  40725  cdleme16d  40727  cdleme17b  40733  cdleme17c  40734  cdleme18c  40739  cdleme18d  40741  cdlemeda  40744  cdlemednpq  40745  cdleme19a  40749  cdleme19c  40751  cdleme20aN  40755  cdleme20bN  40756  cdleme20d  40758  cdleme20f  40760  cdleme20g  40761  cdleme20j  40764  cdleme20l1  40766  cdleme21f  40778  cdleme22aa  40785  cdleme22a  40786  cdleme22cN  40788  cdleme22e  40790  cdleme22f2  40793  cdleme22g  40794  cdleme23b  40796  cdleme23c  40797  cdleme26e  40805  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme28a  40816  cdleme28b  40817  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35h2  40903  cdleme38m  40909  cdleme41sn4aw  40921  cdlemf1  41007  cdlemg1cex  41034  cdlemg2ce  41038  cdlemg4d  41059  cdlemg4f  41061  cdlemg7fvN  41070  cdlemg8a  41073  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg11a  41083  cdlemg11aq  41084  cdlemg10a  41086  cdlemg11b  41088  cdlemg12a  41089  cdlemg12b  41090  cdlemg12d  41092  cdlemg12e  41093  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17b  41108  cdlemg17dN  41109  cdlemg17e  41111  cdlemg17h  41114  cdlemg17pq  41118  cdlemg17iqN  41120  cdlemg18b  41125  cdlemg18c  41126  cdlemg18d  41127  cdlemg18  41128  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg31b0N  41140  cdlemg27b  41142  cdlemg33b0  41147  cdlemg33c0  41148  cdlemg28  41150  cdlemg33a  41152  cdlemg35  41159  cdlemg42  41175  cdlemg44a  41177  cdlemg47  41182  cdlemh2  41262  cdlemh  41263  cdlemj1  41267  cdlemk3  41279  cdlemk5  41282  cdlemki  41287  cdlemksv2  41293  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk16a  41302  cdlemk16  41303  cdlemkj  41309  cdlemkuv2  41313  cdlemk18  41314  cdlemk19  41315  cdlemk7u  41316  cdlemk12u  41318  cdlemkoatnle-2N  41321  cdlemk13-2N  41322  cdlemkole-2N  41323  cdlemk14-2N  41324  cdlemk15-2N  41325  cdlemk16-2N  41326  cdlemk17-2N  41327  cdlemk18-2N  41332  cdlemk19-2N  41333  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk21-2N  41337  cdlemk20-2N  41338  cdlemk22  41339  cdlemk30  41340  cdlemk31  41342  cdlemk32  41343  cdlemk24-3  41349  cdlemkid2  41370  cdlemkfid3N  41371  cdlemk45  41393  cdlemk46  41394  cdlemk47  41395  cdlemk52  41400  cdlemk53a  41401  cdleml1N  41422  cdleml3N  41424  cdlemn7  41649  cdlemn10  41652  dihordlem7  41660  dihord1  41664  dihord2a  41665  dihord10  41669  dihord11c  41670  dihord2pre2  41672  hlhilphllem  42405  fmuldfeq  46013  usgrgrtrirex  48426  grlimprclnbgredg  48473  seposep  49401  iscnrm3rlem8  49422  iscnrm3llem2  49425