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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp133  1309  simp233  1318  simp333  1327  smogt  8207  bitsfzo  16151  frlmphl  20997  mdetunilem4  21773  mdetuni0  21779  mdetmul  21781  decpmatmullem  21929  logexprlim  26382  ax5seg  27315  iocinioc2  31109  bnj966  32933  eqfunresadj  33744  noinfres  33934  cgrtr  34303  cgrtr3  34305  ofscom  34318  segconeq  34321  btwnxfr  34367  colinearxfr  34386  fscgr  34391  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem8  34405  btwnconn1lem9  34406  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn1lem12  34409  brsegle2  34420  seglecgr12im  34421  seglecgr12  34422  segletr  34425  outsideofeq  34441  lshpkrlem5  37135  lshpkrlem6  37136  atbtwnexOLDN  37468  atbtwnex  37469  4noncolr3  37474  3dimlem3a  37481  3dimlem4a  37484  3dim1  37488  3dim2  37489  1cvrat  37497  2atjlej  37500  hlatexch4  37502  ps-2b  37503  2atm  37548  ps-2c  37549  lvolex3N  37559  2atmat  37582  lvolnlelpln  37606  4atlem10  37627  4atlem11b  37629  4atlem11  37630  4at  37634  4at2  37635  2lplnja  37640  2lplnj  37641  dalemclccjdd  37709  paddasslem5  37845  paddasslem15  37855  pmodlem1  37867  dalawlem1  37892  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem15  37906  osumcllem5N  37981  osumcllem6N  37982  lhpexle3lem  38032  lhpmcvr4N  38047  lhpmcvr6N  38049  4atexlemex6  38095  4atex2  38098  4atex2-0bOLDN  38100  4atex3  38102  ltrn11at  38168  cdlemd3  38221  cdleme7aa  38263  cdleme7b  38265  cdleme7c  38266  cdleme7d  38267  cdleme7ga  38269  cdleme16aN  38280  cdleme11dN  38283  cdleme11e  38284  cdleme11l  38290  cdleme11  38291  cdleme12  38292  cdleme14  38294  cdleme15c  38297  cdleme16b  38300  cdleme16d  38302  cdleme17b  38308  cdleme17c  38309  cdleme18c  38314  cdleme18d  38316  cdlemeda  38319  cdlemednpq  38320  cdleme19a  38324  cdleme19c  38326  cdleme20aN  38330  cdleme20bN  38331  cdleme20d  38333  cdleme20f  38335  cdleme20g  38336  cdleme20j  38339  cdleme20l1  38341  cdleme21f  38353  cdleme22aa  38360  cdleme22a  38361  cdleme22cN  38363  cdleme22e  38365  cdleme22f2  38368  cdleme22g  38369  cdleme23b  38371  cdleme23c  38372  cdleme26e  38380  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme28a  38391  cdleme28b  38392  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35h2  38478  cdleme38m  38484  cdleme41sn4aw  38496  cdlemf1  38582  cdlemg1cex  38609  cdlemg2ce  38613  cdlemg4d  38634  cdlemg4f  38636  cdlemg7fvN  38645  cdlemg8a  38648  cdlemg8b  38649  cdlemg8c  38650  cdlemg9a  38653  cdlemg11a  38658  cdlemg11aq  38659  cdlemg10a  38661  cdlemg11b  38663  cdlemg12a  38664  cdlemg12b  38665  cdlemg12d  38667  cdlemg12e  38668  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg13  38673  cdlemg14f  38674  cdlemg14g  38675  cdlemg17b  38683  cdlemg17dN  38684  cdlemg17e  38686  cdlemg17h  38689  cdlemg17pq  38693  cdlemg17iqN  38695  cdlemg18b  38700  cdlemg18c  38701  cdlemg18d  38702  cdlemg18  38703  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg31b0N  38715  cdlemg27b  38717  cdlemg33b0  38722  cdlemg33c0  38723  cdlemg28  38725  cdlemg33a  38727  cdlemg35  38734  cdlemg42  38750  cdlemg44a  38752  cdlemg47  38757  cdlemh2  38837  cdlemh  38838  cdlemj1  38842  cdlemk3  38854  cdlemk5  38857  cdlemki  38862  cdlemksv2  38868  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk16a  38877  cdlemk16  38878  cdlemkj  38884  cdlemkuv2  38888  cdlemk18  38889  cdlemk19  38890  cdlemk7u  38891  cdlemk12u  38893  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk7u-2N  38909  cdlemk11u-2N  38910  cdlemk12u-2N  38911  cdlemk21-2N  38912  cdlemk20-2N  38913  cdlemk22  38914  cdlemk30  38915  cdlemk31  38917  cdlemk32  38918  cdlemk24-3  38924  cdlemkid2  38945  cdlemkfid3N  38946  cdlemk45  38968  cdlemk46  38969  cdlemk47  38970  cdlemk52  38975  cdlemk53a  38976  cdleml1N  38997  cdleml3N  38999  cdlemn7  39224  cdlemn10  39227  dihordlem7  39235  dihord1  39239  dihord2a  39240  dihord10  39244  dihord11c  39245  dihord2pre2  39247  hlhilphllem  39984  fmuldfeq  43131  seposep  46230  iscnrm3rlem8  46252  iscnrm3llem2  46255