Theorem simp33 1212

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 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1135	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  1311  simp233  1320  simp333  1329  eqfunresadj  7289  smogt  8282  bitsfzo  16338  frlmphl  21711  mdetunilem4  22523  mdetuni0  22529  mdetmul  22531  decpmatmullem  22679  logexprlim  27156  noinfres  27654  ax5seg  28909  iocinioc2  32752  bnj966  34946  cgrtr  36005  cgrtr3  36007  ofscom  36020  segconeq  36023  btwnxfr  36069  colinearxfr  36088  fscgr  36093  btwnconn1lem1  36100  btwnconn1lem2  36101  btwnconn1lem5  36104  btwnconn1lem6  36105  btwnconn1lem8  36107  btwnconn1lem9  36108  btwnconn1lem10  36109  btwnconn1lem11  36110  btwnconn1lem12  36111  brsegle2  36122  seglecgr12im  36123  seglecgr12  36124  segletr  36127  outsideofeq  36143  lshpkrlem5  39132  lshpkrlem6  39133  atbtwnexOLDN  39465  atbtwnex  39466  4noncolr3  39471  3dimlem3a  39478  3dimlem4a  39481  3dim1  39485  3dim2  39486  1cvrat  39494  2atjlej  39497  hlatexch4  39499  ps-2b  39500  2atm  39545  ps-2c  39546  lvolex3N  39556  2atmat  39579  lvolnlelpln  39603  4atlem10  39624  4atlem11b  39626  4atlem11  39627  4at  39631  4at2  39632  2lplnja  39637  2lplnj  39638  dalemclccjdd  39706  paddasslem5  39842  paddasslem15  39852  pmodlem1  39864  dalawlem1  39889  dalawlem3  39891  dalawlem4  39892  dalawlem5  39893  dalawlem6  39894  dalawlem7  39895  dalawlem8  39896  dalawlem9  39897  dalawlem11  39899  dalawlem12  39900  dalawlem15  39903  osumcllem5N  39978  osumcllem6N  39979  lhpexle3lem  40029  lhpmcvr4N  40044  lhpmcvr6N  40046  4atexlemex6  40092  4atex2  40095  4atex2-0bOLDN  40097  4atex3  40099  ltrn11at  40165  cdlemd3  40218  cdleme7aa  40260  cdleme7b  40262  cdleme7c  40263  cdleme7d  40264  cdleme7ga  40266  cdleme16aN  40277  cdleme11dN  40280  cdleme11e  40281  cdleme11l  40287  cdleme11  40288  cdleme12  40289  cdleme14  40291  cdleme15c  40294  cdleme16b  40297  cdleme16d  40299  cdleme17b  40305  cdleme17c  40306  cdleme18c  40311  cdleme18d  40313  cdlemeda  40316  cdlemednpq  40317  cdleme19a  40321  cdleme19c  40323  cdleme20aN  40327  cdleme20bN  40328  cdleme20d  40330  cdleme20f  40332  cdleme20g  40333  cdleme20j  40336  cdleme20l1  40338  cdleme21f  40350  cdleme22aa  40357  cdleme22a  40358  cdleme22cN  40360  cdleme22e  40362  cdleme22f2  40365  cdleme22g  40366  cdleme23b  40368  cdleme23c  40369  cdleme26e  40377  cdleme26fALTN  40380  cdleme26f  40381  cdleme26f2ALTN  40382  cdleme26f2  40383  cdleme28a  40388  cdleme28b  40389  cdleme32b  40460  cdleme32c  40461  cdleme32e  40463  cdleme35h2  40475  cdleme38m  40481  cdleme41sn4aw  40493  cdlemf1  40579  cdlemg1cex  40606  cdlemg2ce  40610  cdlemg4d  40631  cdlemg4f  40633  cdlemg7fvN  40642  cdlemg8a  40645  cdlemg8b  40646  cdlemg8c  40647  cdlemg9a  40650  cdlemg11a  40655  cdlemg11aq  40656  cdlemg10a  40658  cdlemg11b  40660  cdlemg12a  40661  cdlemg12b  40662  cdlemg12d  40664  cdlemg12e  40665  cdlemg12f  40666  cdlemg12g  40667  cdlemg12  40668  cdlemg13a  40669  cdlemg13  40670  cdlemg14f  40671  cdlemg14g  40672  cdlemg17b  40680  cdlemg17dN  40681  cdlemg17e  40683  cdlemg17h  40686  cdlemg17pq  40690  cdlemg17iqN  40692  cdlemg18b  40697  cdlemg18c  40698  cdlemg18d  40699  cdlemg18  40700  cdlemg19  40702  cdlemg21  40704  cdlemg27a  40710  cdlemg31b0N  40712  cdlemg27b  40714  cdlemg33b0  40719  cdlemg33c0  40720  cdlemg28  40722  cdlemg33a  40724  cdlemg35  40731  cdlemg42  40747  cdlemg44a  40749  cdlemg47  40754  cdlemh2  40834  cdlemh  40835  cdlemj1  40839  cdlemk3  40851  cdlemk5  40854  cdlemki  40859  cdlemksv2  40865  cdlemk7  40866  cdlemk11  40867  cdlemk12  40868  cdlemkole  40871  cdlemk14  40872  cdlemk15  40873  cdlemk16a  40874  cdlemk16  40875  cdlemkj  40881  cdlemkuv2  40885  cdlemk18  40886  cdlemk19  40887  cdlemk7u  40888  cdlemk12u  40890  cdlemkoatnle-2N  40893  cdlemk13-2N  40894  cdlemkole-2N  40895  cdlemk14-2N  40896  cdlemk15-2N  40897  cdlemk16-2N  40898  cdlemk17-2N  40899  cdlemk18-2N  40904  cdlemk19-2N  40905  cdlemk7u-2N  40906  cdlemk11u-2N  40907  cdlemk12u-2N  40908  cdlemk21-2N  40909  cdlemk20-2N  40910  cdlemk22  40911  cdlemk30  40912  cdlemk31  40914  cdlemk32  40915  cdlemk24-3  40921  cdlemkid2  40942  cdlemkfid3N  40943  cdlemk45  40965  cdlemk46  40966  cdlemk47  40967  cdlemk52  40972  cdlemk53a  40973  cdleml1N  40994  cdleml3N  40996  cdlemn7  41221  cdlemn10  41224  dihordlem7  41232  dihord1  41236  dihord2a  41237  dihord10  41241  dihord11c  41242  dihord2pre2  41244  hlhilphllem  41977  fmuldfeq  45602  usgrgrtrirex  47960  grlimprclnbgredg  48007  seposep  48936  iscnrm3rlem8  48957  iscnrm3llem2  48960