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  7356  smogt  8350  bitsfzo  16489  frlmphl  21896  mdetunilem4  22737  mdetuni0  22743  mdetmul  22745  decpmatmullem  22893  logexprlim  27351  noinfres  27848  ax5seg  29225  iocinioc2  33061  bnj966  35273  cgrtr  36379  cgrtr3  36381  ofscom  36394  segconeq  36397  btwnxfr  36443  colinearxfr  36462  fscgr  36467  btwnconn1lem1  36474  btwnconn1lem2  36475  btwnconn1lem5  36478  btwnconn1lem6  36479  btwnconn1lem8  36481  btwnconn1lem9  36482  btwnconn1lem10  36483  btwnconn1lem11  36484  btwnconn1lem12  36485  brsegle2  36496  seglecgr12im  36497  seglecgr12  36498  segletr  36501  outsideofeq  36517  lshpkrlem5  39773  lshpkrlem6  39774  atbtwnexOLDN  40106  atbtwnex  40107  4noncolr3  40112  3dimlem3a  40119  3dimlem4a  40122  3dim1  40126  3dim2  40127  1cvrat  40135  2atjlej  40138  hlatexch4  40140  ps-2b  40141  2atm  40186  ps-2c  40187  lvolex3N  40197  2atmat  40220  lvolnlelpln  40244  4atlem10  40265  4atlem11b  40267  4atlem11  40268  4at  40272  4at2  40273  2lplnja  40278  2lplnj  40279  dalemclccjdd  40347  paddasslem5  40483  paddasslem15  40493  pmodlem1  40505  dalawlem1  40530  dalawlem3  40532  dalawlem4  40533  dalawlem5  40534  dalawlem6  40535  dalawlem7  40536  dalawlem8  40537  dalawlem9  40538  dalawlem11  40540  dalawlem12  40541  dalawlem15  40544  osumcllem5N  40619  osumcllem6N  40620  lhpexle3lem  40670  lhpmcvr4N  40685  lhpmcvr6N  40687  4atexlemex6  40733  4atex2  40736  4atex2-0bOLDN  40738  4atex3  40740  ltrn11at  40806  cdlemd3  40859  cdleme7aa  40901  cdleme7b  40903  cdleme7c  40904  cdleme7d  40905  cdleme7ga  40907  cdleme16aN  40918  cdleme11dN  40921  cdleme11e  40922  cdleme11l  40928  cdleme11  40929  cdleme12  40930  cdleme14  40932  cdleme15c  40935  cdleme16b  40938  cdleme16d  40940  cdleme17b  40946  cdleme17c  40947  cdleme18c  40952  cdleme18d  40954  cdlemeda  40957  cdlemednpq  40958  cdleme19a  40962  cdleme19c  40964  cdleme20aN  40968  cdleme20bN  40969  cdleme20d  40971  cdleme20f  40973  cdleme20g  40974  cdleme20j  40977  cdleme20l1  40979  cdleme21f  40991  cdleme22aa  40998  cdleme22a  40999  cdleme22cN  41001  cdleme22e  41003  cdleme22f2  41006  cdleme22g  41007  cdleme23b  41009  cdleme23c  41010  cdleme26e  41018  cdleme26fALTN  41021  cdleme26f  41022  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme28a  41029  cdleme28b  41030  cdleme32b  41101  cdleme32c  41102  cdleme32e  41104  cdleme35h2  41116  cdleme38m  41122  cdleme41sn4aw  41134  cdlemf1  41220  cdlemg1cex  41247  cdlemg2ce  41251  cdlemg4d  41272  cdlemg4f  41274  cdlemg7fvN  41283  cdlemg8a  41286  cdlemg8b  41287  cdlemg8c  41288  cdlemg9a  41291  cdlemg11a  41296  cdlemg11aq  41297  cdlemg10a  41299  cdlemg11b  41301  cdlemg12a  41302  cdlemg12b  41303  cdlemg12d  41305  cdlemg12e  41306  cdlemg12f  41307  cdlemg12g  41308  cdlemg12  41309  cdlemg13a  41310  cdlemg13  41311  cdlemg14f  41312  cdlemg14g  41313  cdlemg17b  41321  cdlemg17dN  41322  cdlemg17e  41324  cdlemg17h  41327  cdlemg17pq  41331  cdlemg17iqN  41333  cdlemg18b  41338  cdlemg18c  41339  cdlemg18d  41340  cdlemg18  41341  cdlemg19  41343  cdlemg21  41345  cdlemg27a  41351  cdlemg31b0N  41353  cdlemg27b  41355  cdlemg33b0  41360  cdlemg33c0  41361  cdlemg28  41363  cdlemg33a  41365  cdlemg35  41372  cdlemg42  41388  cdlemg44a  41390  cdlemg47  41395  cdlemh2  41475  cdlemh  41476  cdlemj1  41480  cdlemk3  41492  cdlemk5  41495  cdlemki  41500  cdlemksv2  41506  cdlemk7  41507  cdlemk11  41508  cdlemk12  41509  cdlemkole  41512  cdlemk14  41513  cdlemk15  41514  cdlemk16a  41515  cdlemk16  41516  cdlemkj  41522  cdlemkuv2  41526  cdlemk18  41527  cdlemk19  41528  cdlemk7u  41529  cdlemk12u  41531  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk7u-2N  41547  cdlemk11u-2N  41548  cdlemk12u-2N  41549  cdlemk21-2N  41550  cdlemk20-2N  41551  cdlemk22  41552  cdlemk30  41553  cdlemk31  41555  cdlemk32  41556  cdlemk24-3  41562  cdlemkid2  41583  cdlemkfid3N  41584  cdlemk45  41606  cdlemk46  41607  cdlemk47  41608  cdlemk52  41613  cdlemk53a  41614  cdleml1N  41635  cdleml3N  41637  cdlemn7  41862  cdlemn10  41865  dihordlem7  41873  dihord1  41877  dihord2a  41878  dihord10  41882  dihord11c  41883  dihord2pre2  41885  hlhilphllem  42618  fmuldfeq  46186  usgrgrtrirex  48599  grlimprclnbgredg  48646  seposep  49584  iscnrm3rlem8  49605  iscnrm3llem2  49608