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 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp133  1329  simp233  1338  simp333  1347  eqfunresadj  7372  smogt  8380  bitsfzo  16612  frlmphl  22094  mdetunilem4  22937  mdetuni0  22943  mdetmul  22945  decpmatmullem  23096  logexprlim  27559  noinfres  28086  ax5seg  29523  iocinioc2  33419  bnj966  35622  cgrtr  36851  cgrtr3  36853  ofscom  36866  segconeq  36869  btwnxfr  36915  colinearxfr  36934  fscgr  36939  btwnconn1lem1  36946  btwnconn1lem2  36947  btwnconn1lem5  36950  btwnconn1lem6  36951  btwnconn1lem8  36953  btwnconn1lem9  36954  btwnconn1lem10  36955  btwnconn1lem11  36956  btwnconn1lem12  36957  brsegle2  36968  seglecgr12im  36969  seglecgr12  36970  segletr  36973  outsideofeq  36989  lshpkrlem5  40278  lshpkrlem6  40279  atbtwnexOLDN  40611  atbtwnex  40612  4noncolr3  40617  3dimlem3a  40624  3dimlem4a  40627  3dim1  40631  3dim2  40632  1cvrat  40640  2atjlej  40643  hlatexch4  40645  ps-2b  40646  2atm  40691  ps-2c  40692  lvolex3N  40702  2atmat  40725  lvolnlelpln  40749  4atlem10  40770  4atlem11b  40772  4atlem11  40773  4at  40777  4at2  40778  2lplnja  40783  2lplnj  40784  dalemclccjdd  40852  paddasslem5  40988  paddasslem15  40998  pmodlem1  41010  dalawlem1  41035  dalawlem3  41037  dalawlem4  41038  dalawlem5  41039  dalawlem6  41040  dalawlem7  41041  dalawlem8  41042  dalawlem9  41043  dalawlem11  41045  dalawlem12  41046  dalawlem15  41049  osumcllem5N  41124  osumcllem6N  41125  lhpexle3lem  41175  lhpmcvr4N  41190  lhpmcvr6N  41192  4atexlemex6  41238  4atex2  41241  4atex2-0bOLDN  41243  4atex3  41245  ltrn11at  41311  cdlemd3  41364  cdleme7aa  41406  cdleme7b  41408  cdleme7c  41409  cdleme7d  41410  cdleme7ga  41412  cdleme16aN  41423  cdleme11dN  41426  cdleme11e  41427  cdleme11l  41433  cdleme11  41434  cdleme12  41435  cdleme14  41437  cdleme15c  41440  cdleme16b  41443  cdleme16d  41445  cdleme17b  41451  cdleme17c  41452  cdleme18c  41457  cdleme18d  41459  cdlemeda  41462  cdlemednpq  41463  cdleme19a  41467  cdleme19c  41469  cdleme20aN  41473  cdleme20bN  41474  cdleme20d  41476  cdleme20f  41478  cdleme20g  41479  cdleme20j  41482  cdleme20l1  41484  cdleme21f  41496  cdleme22aa  41503  cdleme22a  41504  cdleme22cN  41506  cdleme22e  41508  cdleme22f2  41511  cdleme22g  41512  cdleme23b  41514  cdleme23c  41515  cdleme26e  41523  cdleme26fALTN  41526  cdleme26f  41527  cdleme26f2ALTN  41528  cdleme26f2  41529  cdleme28a  41534  cdleme28b  41535  cdleme32b  41606  cdleme32c  41607  cdleme32e  41609  cdleme35h2  41621  cdleme38m  41627  cdleme41sn4aw  41639  cdlemf1  41725  cdlemg1cex  41752  cdlemg2ce  41756  cdlemg4d  41777  cdlemg4f  41779  cdlemg7fvN  41788  cdlemg8a  41791  cdlemg8b  41792  cdlemg8c  41793  cdlemg9a  41796  cdlemg11a  41801  cdlemg11aq  41802  cdlemg10a  41804  cdlemg11b  41806  cdlemg12a  41807  cdlemg12b  41808  cdlemg12d  41810  cdlemg12e  41811  cdlemg12f  41812  cdlemg12g  41813  cdlemg12  41814  cdlemg13a  41815  cdlemg13  41816  cdlemg14f  41817  cdlemg14g  41818  cdlemg17b  41826  cdlemg17dN  41827  cdlemg17e  41829  cdlemg17h  41832  cdlemg17pq  41836  cdlemg17iqN  41838  cdlemg18b  41843  cdlemg18c  41844  cdlemg18d  41845  cdlemg18  41846  cdlemg19  41848  cdlemg21  41850  cdlemg27a  41856  cdlemg31b0N  41858  cdlemg27b  41860  cdlemg33b0  41865  cdlemg33c0  41866  cdlemg28  41868  cdlemg33a  41870  cdlemg35  41877  cdlemg42  41893  cdlemg44a  41895  cdlemg47  41900  cdlemh2  41980  cdlemh  41981  cdlemj1  41985  cdlemk3  41997  cdlemk5  42000  cdlemki  42005  cdlemksv2  42011  cdlemk7  42012  cdlemk11  42013  cdlemk12  42014  cdlemkole  42017  cdlemk14  42018  cdlemk15  42019  cdlemk16a  42020  cdlemk16  42021  cdlemkj  42027  cdlemkuv2  42031  cdlemk18  42032  cdlemk19  42033  cdlemk7u  42034  cdlemk12u  42036  cdlemkoatnle-2N  42039  cdlemk13-2N  42040  cdlemkole-2N  42041  cdlemk14-2N  42042  cdlemk15-2N  42043  cdlemk16-2N  42044  cdlemk17-2N  42045  cdlemk18-2N  42050  cdlemk19-2N  42051  cdlemk7u-2N  42052  cdlemk11u-2N  42053  cdlemk12u-2N  42054  cdlemk21-2N  42055  cdlemk20-2N  42056  cdlemk22  42057  cdlemk30  42058  cdlemk31  42060  cdlemk32  42061  cdlemk24-3  42067  cdlemkid2  42088  cdlemkfid3N  42089  cdlemk45  42111  cdlemk46  42112  cdlemk47  42113  cdlemk52  42118  cdlemk53a  42119  cdleml1N  42140  cdleml3N  42142  cdlemn7  42367  cdlemn10  42370  dihordlem7  42378  dihord1  42382  dihord2a  42383  dihord10  42387  dihord11c  42388  dihord2pre2  42390  hlhilphllem  43123  fmuldfeq  46702  usgrgrtrirex  49155  grlimprclnbgredg  49202  seposep  50147  iscnrm3rlem8  50168  iscnrm3llem2  50171