Theorem simp33 1210

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp133  1309  simp233  1318  simp333  1327  eqfunresadj  7379  smogt  8405  bitsfzo  16468  frlmphl  21818  mdetunilem4  22636  mdetuni0  22642  mdetmul  22644  decpmatmullem  22792  logexprlim  27283  noinfres  27781  ax5seg  28967  iocinioc2  32787  bnj966  34936  cgrtr  35973  cgrtr3  35975  ofscom  35988  segconeq  35991  btwnxfr  36037  colinearxfr  36056  fscgr  36061  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  brsegle2  36090  seglecgr12im  36091  seglecgr12  36092  segletr  36095  outsideofeq  36111  lshpkrlem5  39095  lshpkrlem6  39096  atbtwnexOLDN  39429  atbtwnex  39430  4noncolr3  39435  3dimlem3a  39442  3dimlem4a  39445  3dim1  39449  3dim2  39450  1cvrat  39458  2atjlej  39461  hlatexch4  39463  ps-2b  39464  2atm  39509  ps-2c  39510  lvolex3N  39520  2atmat  39543  lvolnlelpln  39567  4atlem10  39588  4atlem11b  39590  4atlem11  39591  4at  39595  4at2  39596  2lplnja  39601  2lplnj  39602  dalemclccjdd  39670  paddasslem5  39806  paddasslem15  39816  pmodlem1  39828  dalawlem1  39853  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem15  39867  osumcllem5N  39942  osumcllem6N  39943  lhpexle3lem  39993  lhpmcvr4N  40008  lhpmcvr6N  40010  4atexlemex6  40056  4atex2  40059  4atex2-0bOLDN  40061  4atex3  40063  ltrn11at  40129  cdlemd3  40182  cdleme7aa  40224  cdleme7b  40226  cdleme7c  40227  cdleme7d  40228  cdleme7ga  40230  cdleme16aN  40241  cdleme11dN  40244  cdleme11e  40245  cdleme11l  40251  cdleme11  40252  cdleme12  40253  cdleme14  40255  cdleme15c  40258  cdleme16b  40261  cdleme16d  40263  cdleme17b  40269  cdleme17c  40270  cdleme18c  40275  cdleme18d  40277  cdlemeda  40280  cdlemednpq  40281  cdleme19a  40285  cdleme19c  40287  cdleme20aN  40291  cdleme20bN  40292  cdleme20d  40294  cdleme20f  40296  cdleme20g  40297  cdleme20j  40300  cdleme20l1  40302  cdleme21f  40314  cdleme22aa  40321  cdleme22a  40322  cdleme22cN  40324  cdleme22e  40326  cdleme22f2  40329  cdleme22g  40330  cdleme23b  40332  cdleme23c  40333  cdleme26e  40341  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme28a  40352  cdleme28b  40353  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35h2  40439  cdleme38m  40445  cdleme41sn4aw  40457  cdlemf1  40543  cdlemg1cex  40570  cdlemg2ce  40574  cdlemg4d  40595  cdlemg4f  40597  cdlemg7fvN  40606  cdlemg8a  40609  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg11a  40619  cdlemg11aq  40620  cdlemg10a  40622  cdlemg11b  40624  cdlemg12a  40625  cdlemg12b  40626  cdlemg12d  40628  cdlemg12e  40629  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17b  40644  cdlemg17dN  40645  cdlemg17e  40647  cdlemg17h  40650  cdlemg17pq  40654  cdlemg17iqN  40656  cdlemg18b  40661  cdlemg18c  40662  cdlemg18d  40663  cdlemg18  40664  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg31b0N  40676  cdlemg27b  40678  cdlemg33b0  40683  cdlemg33c0  40684  cdlemg28  40686  cdlemg33a  40688  cdlemg35  40695  cdlemg42  40711  cdlemg44a  40713  cdlemg47  40718  cdlemh2  40798  cdlemh  40799  cdlemj1  40803  cdlemk3  40815  cdlemk5  40818  cdlemki  40823  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk16a  40838  cdlemk16  40839  cdlemkj  40845  cdlemkuv2  40849  cdlemk18  40850  cdlemk19  40851  cdlemk7u  40852  cdlemk12u  40854  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk21-2N  40873  cdlemk20-2N  40874  cdlemk22  40875  cdlemk30  40876  cdlemk31  40878  cdlemk32  40879  cdlemk24-3  40885  cdlemkid2  40906  cdlemkfid3N  40907  cdlemk45  40929  cdlemk46  40930  cdlemk47  40931  cdlemk52  40936  cdlemk53a  40937  cdleml1N  40958  cdleml3N  40960  cdlemn7  41185  cdlemn10  41188  dihordlem7  41196  dihord1  41200  dihord2a  41201  dihord10  41205  dihord11c  41206  dihord2pre2  41208  hlhilphllem  41945  fmuldfeq  45538  usgrgrtrirex  47852  seposep  48721  iscnrm3rlem8  48743  iscnrm3llem2  48746