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  7366  smogt  8356  bitsfzo  16511  frlmphl  21961  mdetunilem4  22802  mdetuni0  22808  mdetmul  22810  decpmatmullem  22958  logexprlim  27420  noinfres  27917  ax5seg  29319  iocinioc2  33170  bnj966  35373  cgrtr  36497  cgrtr3  36499  ofscom  36512  segconeq  36515  btwnxfr  36561  colinearxfr  36580  fscgr  36585  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem5  36596  btwnconn1lem6  36597  btwnconn1lem8  36599  btwnconn1lem9  36600  btwnconn1lem10  36601  btwnconn1lem11  36602  btwnconn1lem12  36603  brsegle2  36614  seglecgr12im  36615  seglecgr12  36616  segletr  36619  outsideofeq  36635  lshpkrlem5  39921  lshpkrlem6  39922  atbtwnexOLDN  40254  atbtwnex  40255  4noncolr3  40260  3dimlem3a  40267  3dimlem4a  40270  3dim1  40274  3dim2  40275  1cvrat  40283  2atjlej  40286  hlatexch4  40288  ps-2b  40289  2atm  40334  ps-2c  40335  lvolex3N  40345  2atmat  40368  lvolnlelpln  40392  4atlem10  40413  4atlem11b  40415  4atlem11  40416  4at  40420  4at2  40421  2lplnja  40426  2lplnj  40427  dalemclccjdd  40495  paddasslem5  40631  paddasslem15  40641  pmodlem1  40653  dalawlem1  40678  dalawlem3  40680  dalawlem4  40681  dalawlem5  40682  dalawlem6  40683  dalawlem7  40684  dalawlem8  40685  dalawlem9  40686  dalawlem11  40688  dalawlem12  40689  dalawlem15  40692  osumcllem5N  40767  osumcllem6N  40768  lhpexle3lem  40818  lhpmcvr4N  40833  lhpmcvr6N  40835  4atexlemex6  40881  4atex2  40884  4atex2-0bOLDN  40886  4atex3  40888  ltrn11at  40954  cdlemd3  41007  cdleme7aa  41049  cdleme7b  41051  cdleme7c  41052  cdleme7d  41053  cdleme7ga  41055  cdleme16aN  41066  cdleme11dN  41069  cdleme11e  41070  cdleme11l  41076  cdleme11  41077  cdleme12  41078  cdleme14  41080  cdleme15c  41083  cdleme16b  41086  cdleme16d  41088  cdleme17b  41094  cdleme17c  41095  cdleme18c  41100  cdleme18d  41102  cdlemeda  41105  cdlemednpq  41106  cdleme19a  41110  cdleme19c  41112  cdleme20aN  41116  cdleme20bN  41117  cdleme20d  41119  cdleme20f  41121  cdleme20g  41122  cdleme20j  41125  cdleme20l1  41127  cdleme21f  41139  cdleme22aa  41146  cdleme22a  41147  cdleme22cN  41149  cdleme22e  41151  cdleme22f2  41154  cdleme22g  41155  cdleme23b  41157  cdleme23c  41158  cdleme26e  41166  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme28a  41177  cdleme28b  41178  cdleme32b  41249  cdleme32c  41250  cdleme32e  41252  cdleme35h2  41264  cdleme38m  41270  cdleme41sn4aw  41282  cdlemf1  41368  cdlemg1cex  41395  cdlemg2ce  41399  cdlemg4d  41420  cdlemg4f  41422  cdlemg7fvN  41431  cdlemg8a  41434  cdlemg8b  41435  cdlemg8c  41436  cdlemg9a  41439  cdlemg11a  41444  cdlemg11aq  41445  cdlemg10a  41447  cdlemg11b  41449  cdlemg12a  41450  cdlemg12b  41451  cdlemg12d  41453  cdlemg12e  41454  cdlemg12f  41455  cdlemg12g  41456  cdlemg12  41457  cdlemg13a  41458  cdlemg13  41459  cdlemg14f  41460  cdlemg14g  41461  cdlemg17b  41469  cdlemg17dN  41470  cdlemg17e  41472  cdlemg17h  41475  cdlemg17pq  41479  cdlemg17iqN  41481  cdlemg18b  41486  cdlemg18c  41487  cdlemg18d  41488  cdlemg18  41489  cdlemg19  41491  cdlemg21  41493  cdlemg27a  41499  cdlemg31b0N  41501  cdlemg27b  41503  cdlemg33b0  41508  cdlemg33c0  41509  cdlemg28  41511  cdlemg33a  41513  cdlemg35  41520  cdlemg42  41536  cdlemg44a  41538  cdlemg47  41543  cdlemh2  41623  cdlemh  41624  cdlemj1  41628  cdlemk3  41640  cdlemk5  41643  cdlemki  41648  cdlemksv2  41654  cdlemk7  41655  cdlemk11  41656  cdlemk12  41657  cdlemkole  41660  cdlemk14  41661  cdlemk15  41662  cdlemk16a  41663  cdlemk16  41664  cdlemkj  41670  cdlemkuv2  41674  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk12u  41679  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk12u-2N  41697  cdlemk21-2N  41698  cdlemk20-2N  41699  cdlemk22  41700  cdlemk30  41701  cdlemk31  41703  cdlemk32  41704  cdlemk24-3  41710  cdlemkid2  41731  cdlemkfid3N  41732  cdlemk45  41754  cdlemk46  41755  cdlemk47  41756  cdlemk52  41761  cdlemk53a  41762  cdleml1N  41783  cdleml3N  41785  cdlemn7  42010  cdlemn10  42013  dihordlem7  42021  dihord1  42025  dihord2a  42026  dihord10  42030  dihord11c  42031  dihord2pre2  42033  hlhilphllem  42766  fmuldfeq  46332  usgrgrtrirex  48748  grlimprclnbgredg  48795  seposep  49737  iscnrm3rlem8  49758  iscnrm3llem2  49761