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  7401  smogt  8413  bitsfzo  16649  frlmphl  22142  mdetunilem4  22985  mdetuni0  22991  mdetmul  22993  decpmatmullem  23144  logexprlim  27609  noinfres  28136  ax5seg  29573  iocinioc2  33467  bnj966  35685  cgrtr  36972  cgrtr3  36974  ofscom  36987  segconeq  36990  btwnxfr  37036  colinearxfr  37055  fscgr  37060  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem5  37071  btwnconn1lem6  37072  btwnconn1lem8  37074  btwnconn1lem9  37075  btwnconn1lem10  37076  btwnconn1lem11  37077  btwnconn1lem12  37078  brsegle2  37089  seglecgr12im  37090  seglecgr12  37091  segletr  37094  outsideofeq  37110  lshpkrlem5  40437  lshpkrlem6  40438  atbtwnexOLDN  40770  atbtwnex  40771  4noncolr3  40776  3dimlem3a  40783  3dimlem4a  40786  3dim1  40790  3dim2  40791  1cvrat  40799  2atjlej  40802  hlatexch4  40804  ps-2b  40805  2atm  40850  ps-2c  40851  lvolex3N  40861  2atmat  40884  lvolnlelpln  40908  4atlem10  40929  4atlem11b  40931  4atlem11  40932  4at  40936  4at2  40937  2lplnja  40942  2lplnj  40943  dalemclccjdd  41011  paddasslem5  41147  paddasslem15  41157  pmodlem1  41169  dalawlem1  41194  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  osumcllem5N  41283  osumcllem6N  41284  lhpexle3lem  41334  lhpmcvr4N  41349  lhpmcvr6N  41351  4atexlemex6  41397  4atex2  41400  4atex2-0bOLDN  41402  4atex3  41404  ltrn11at  41470  cdlemd3  41523  cdleme7aa  41565  cdleme7b  41567  cdleme7c  41568  cdleme7d  41569  cdleme7ga  41571  cdleme16aN  41582  cdleme11dN  41585  cdleme11e  41586  cdleme11l  41592  cdleme11  41593  cdleme12  41594  cdleme14  41596  cdleme15c  41599  cdleme16b  41602  cdleme16d  41604  cdleme17b  41610  cdleme17c  41611  cdleme18c  41616  cdleme18d  41618  cdlemeda  41621  cdlemednpq  41622  cdleme19a  41626  cdleme19c  41628  cdleme20aN  41632  cdleme20bN  41633  cdleme20d  41635  cdleme20f  41637  cdleme20g  41638  cdleme20j  41641  cdleme20l1  41643  cdleme21f  41655  cdleme22aa  41662  cdleme22a  41663  cdleme22cN  41665  cdleme22e  41667  cdleme22f2  41670  cdleme22g  41671  cdleme23b  41673  cdleme23c  41674  cdleme26e  41682  cdleme26fALTN  41685  cdleme26f  41686  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme28a  41693  cdleme28b  41694  cdleme32b  41765  cdleme32c  41766  cdleme32e  41768  cdleme35h2  41780  cdleme38m  41786  cdleme41sn4aw  41798  cdlemf1  41884  cdlemg1cex  41911  cdlemg2ce  41915  cdlemg4d  41936  cdlemg4f  41938  cdlemg7fvN  41947  cdlemg8a  41950  cdlemg8b  41951  cdlemg8c  41952  cdlemg9a  41955  cdlemg11a  41960  cdlemg11aq  41961  cdlemg10a  41963  cdlemg11b  41965  cdlemg12a  41966  cdlemg12b  41967  cdlemg12d  41969  cdlemg12e  41970  cdlemg12f  41971  cdlemg12g  41972  cdlemg12  41973  cdlemg13a  41974  cdlemg13  41975  cdlemg14f  41976  cdlemg14g  41977  cdlemg17b  41985  cdlemg17dN  41986  cdlemg17e  41988  cdlemg17h  41991  cdlemg17pq  41995  cdlemg17iqN  41997  cdlemg18b  42002  cdlemg18c  42003  cdlemg18d  42004  cdlemg18  42005  cdlemg19  42007  cdlemg21  42009  cdlemg27a  42015  cdlemg31b0N  42017  cdlemg27b  42019  cdlemg33b0  42024  cdlemg33c0  42025  cdlemg28  42027  cdlemg33a  42029  cdlemg35  42036  cdlemg42  42052  cdlemg44a  42054  cdlemg47  42059  cdlemh2  42139  cdlemh  42140  cdlemj1  42144  cdlemk3  42156  cdlemk5  42159  cdlemki  42164  cdlemksv2  42170  cdlemk7  42171  cdlemk11  42172  cdlemk12  42173  cdlemkole  42176  cdlemk14  42177  cdlemk15  42178  cdlemk16a  42179  cdlemk16  42180  cdlemkj  42186  cdlemkuv2  42190  cdlemk18  42191  cdlemk19  42192  cdlemk7u  42193  cdlemk12u  42195  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk7u-2N  42211  cdlemk11u-2N  42212  cdlemk12u-2N  42213  cdlemk21-2N  42214  cdlemk20-2N  42215  cdlemk22  42216  cdlemk30  42217  cdlemk31  42219  cdlemk32  42220  cdlemk24-3  42226  cdlemkid2  42247  cdlemkfid3N  42248  cdlemk45  42270  cdlemk46  42271  cdlemk47  42272  cdlemk52  42277  cdlemk53a  42278  cdleml1N  42299  cdleml3N  42301  cdlemn7  42526  cdlemn10  42529  dihordlem7  42537  dihord1  42541  dihord2a  42542  dihord10  42546  dihord11c  42547  dihord2pre2  42549  hlhilphllem  43282  fmuldfeq  46868  usgrgrtrirex  49321  grlimprclnbgredg  49368  seposep  50371  iscnrm3rlem8  50392  iscnrm3llem2  50395