Theorem simp33 1228

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  simp133  1327  simp233  1336  simp333  1345  eqfunresadj  7359  smogt  8354  bitsfzo  16493  frlmphl  21900  mdetunilem4  22741  mdetuni0  22747  mdetmul  22749  decpmatmullem  22897  logexprlim  27355  noinfres  27852  ax5seg  29229  iocinioc2  33065  bnj966  35277  cgrtr  36417  cgrtr3  36419  ofscom  36432  segconeq  36435  btwnxfr  36481  colinearxfr  36500  fscgr  36505  btwnconn1lem1  36512  btwnconn1lem2  36513  btwnconn1lem5  36516  btwnconn1lem6  36517  btwnconn1lem8  36519  btwnconn1lem9  36520  btwnconn1lem10  36521  btwnconn1lem11  36522  btwnconn1lem12  36523  brsegle2  36534  seglecgr12im  36535  seglecgr12  36536  segletr  36539  outsideofeq  36555  lshpkrlem5  39812  lshpkrlem6  39813  atbtwnexOLDN  40145  atbtwnex  40146  4noncolr3  40151  3dimlem3a  40158  3dimlem4a  40161  3dim1  40165  3dim2  40166  1cvrat  40174  2atjlej  40177  hlatexch4  40179  ps-2b  40180  2atm  40225  ps-2c  40226  lvolex3N  40236  2atmat  40259  lvolnlelpln  40283  4atlem10  40304  4atlem11b  40306  4atlem11  40307  4at  40311  4at2  40312  2lplnja  40317  2lplnj  40318  dalemclccjdd  40386  paddasslem5  40522  paddasslem15  40532  pmodlem1  40544  dalawlem1  40569  dalawlem3  40571  dalawlem4  40572  dalawlem5  40573  dalawlem6  40574  dalawlem7  40575  dalawlem8  40576  dalawlem9  40577  dalawlem11  40579  dalawlem12  40580  dalawlem15  40583  osumcllem5N  40658  osumcllem6N  40659  lhpexle3lem  40709  lhpmcvr4N  40724  lhpmcvr6N  40726  4atexlemex6  40772  4atex2  40775  4atex2-0bOLDN  40777  4atex3  40779  ltrn11at  40845  cdlemd3  40898  cdleme7aa  40940  cdleme7b  40942  cdleme7c  40943  cdleme7d  40944  cdleme7ga  40946  cdleme16aN  40957  cdleme11dN  40960  cdleme11e  40961  cdleme11l  40967  cdleme11  40968  cdleme12  40969  cdleme14  40971  cdleme15c  40974  cdleme16b  40977  cdleme16d  40979  cdleme17b  40985  cdleme17c  40986  cdleme18c  40991  cdleme18d  40993  cdlemeda  40996  cdlemednpq  40997  cdleme19a  41001  cdleme19c  41003  cdleme20aN  41007  cdleme20bN  41008  cdleme20d  41010  cdleme20f  41012  cdleme20g  41013  cdleme20j  41016  cdleme20l1  41018  cdleme21f  41030  cdleme22aa  41037  cdleme22a  41038  cdleme22cN  41040  cdleme22e  41042  cdleme22f2  41045  cdleme22g  41046  cdleme23b  41048  cdleme23c  41049  cdleme26e  41057  cdleme26fALTN  41060  cdleme26f  41061  cdleme26f2ALTN  41062  cdleme26f2  41063  cdleme28a  41068  cdleme28b  41069  cdleme32b  41140  cdleme32c  41141  cdleme32e  41143  cdleme35h2  41155  cdleme38m  41161  cdleme41sn4aw  41173  cdlemf1  41259  cdlemg1cex  41286  cdlemg2ce  41290  cdlemg4d  41311  cdlemg4f  41313  cdlemg7fvN  41322  cdlemg8a  41325  cdlemg8b  41326  cdlemg8c  41327  cdlemg9a  41330  cdlemg11a  41335  cdlemg11aq  41336  cdlemg10a  41338  cdlemg11b  41340  cdlemg12a  41341  cdlemg12b  41342  cdlemg12d  41344  cdlemg12e  41345  cdlemg12f  41346  cdlemg12g  41347  cdlemg12  41348  cdlemg13a  41349  cdlemg13  41350  cdlemg14f  41351  cdlemg14g  41352  cdlemg17b  41360  cdlemg17dN  41361  cdlemg17e  41363  cdlemg17h  41366  cdlemg17pq  41370  cdlemg17iqN  41372  cdlemg18b  41377  cdlemg18c  41378  cdlemg18d  41379  cdlemg18  41380  cdlemg19  41382  cdlemg21  41384  cdlemg27a  41390  cdlemg31b0N  41392  cdlemg27b  41394  cdlemg33b0  41399  cdlemg33c0  41400  cdlemg28  41402  cdlemg33a  41404  cdlemg35  41411  cdlemg42  41427  cdlemg44a  41429  cdlemg47  41434  cdlemh2  41514  cdlemh  41515  cdlemj1  41519  cdlemk3  41531  cdlemk5  41534  cdlemki  41539  cdlemksv2  41545  cdlemk7  41546  cdlemk11  41547  cdlemk12  41548  cdlemkole  41551  cdlemk14  41552  cdlemk15  41553  cdlemk16a  41554  cdlemk16  41555  cdlemkj  41561  cdlemkuv2  41565  cdlemk18  41566  cdlemk19  41567  cdlemk7u  41568  cdlemk12u  41570  cdlemkoatnle-2N  41573  cdlemk13-2N  41574  cdlemkole-2N  41575  cdlemk14-2N  41576  cdlemk15-2N  41577  cdlemk16-2N  41578  cdlemk17-2N  41579  cdlemk18-2N  41584  cdlemk19-2N  41585  cdlemk7u-2N  41586  cdlemk11u-2N  41587  cdlemk12u-2N  41588  cdlemk21-2N  41589  cdlemk20-2N  41590  cdlemk22  41591  cdlemk30  41592  cdlemk31  41594  cdlemk32  41595  cdlemk24-3  41601  cdlemkid2  41622  cdlemkfid3N  41623  cdlemk45  41645  cdlemk46  41646  cdlemk47  41647  cdlemk52  41652  cdlemk53a  41653  cdleml1N  41674  cdleml3N  41676  cdlemn7  41901  cdlemn10  41904  dihordlem7  41912  dihord1  41916  dihord2a  41917  dihord10  41921  dihord11c  41922  dihord2pre2  41924  hlhilphllem  42657  fmuldfeq  46225  usgrgrtrirex  48638  grlimprclnbgredg  48685  seposep  49623  iscnrm3rlem8  49644  iscnrm3llem2  49647