Theorem simp32 1207

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp32	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1134	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1132	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  simp132  1306  simp232  1315  simp332  1324  smogt  7987  axdc3lem4  9864  bitsfzo  15774  frlmphl  20470  mdetunilem4  21220  mdetuni0  21226  mdetmul  21228  decpmatmullem  21376  logfacbnd3  25807  logexprlim  25809  log2sumbnd  26128  ax5seg  26732  numclwwlk1lem2foa  28139  iocinioc2  30528  totprob  31795  eqfunresadj  33117  nosupfv  33319  nosupres  33320  cgrtr  33566  cgrtr3  33568  ofscom  33581  cgrextend  33582  segconeq  33584  ifscgr  33618  colinearxfr  33649  brofs2  33651  brifs2  33652  fscgr  33654  btwnconn1lem2  33662  btwnconn1lem9  33669  btwnconn1lem10  33670  btwnconn1lem11  33671  btwnconn1lem12  33672  brsegle2  33683  seglecgr12im  33684  seglecgr12  33685  segletr  33688  outsideofeq  33704  ivthALT  33796  lshpkrlem5  36410  lshpkrlem6  36411  atbtwnexOLDN  36743  atbtwnex  36744  4noncolr3  36749  3dimlem3a  36756  3dim1  36763  3dim2  36764  1cvrat  36772  2atjlej  36775  hlatexch4  36777  ps-2b  36778  2atm  36823  ps-2c  36824  2atmat  36857  4atlem10  36902  4atlem11b  36904  4atlem11  36905  4at  36909  4at2  36910  2lplnja  36915  2lplnj  36916  dalemswapyz  36952  dalem-ddly  36982  cdlemb  37090  paddasslem5  37120  pmodlem1  37142  dalawlem1  37167  dalawlem3  37169  dalawlem4  37170  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem9  37175  dalawlem11  37177  dalawlem12  37178  dalawlem15  37181  osumcllem5N  37256  osumcllem6N  37257  lhpexle3lem  37307  lhpmcvr4N  37322  lhpmcvr6N  37324  4atexlemex6  37370  4atex2  37373  4atex2-0bOLDN  37375  4atex2-0cOLDN  37376  ltrn11at  37443  trlval3  37483  cdlemd3  37496  cdleme7aa  37538  cdleme7b  37540  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme16aN  37555  cdleme11dN  37558  cdleme11e  37559  cdleme11l  37565  cdleme11  37566  cdleme12  37567  cdleme14  37569  cdleme15a  37570  cdleme15c  37572  cdleme16c  37576  cdleme16d  37577  cdleme16e  37578  cdleme16f  37579  cdleme17c  37584  cdleme18c  37589  cdlemeda  37594  cdlemednpq  37595  cdleme19a  37599  cdleme19c  37601  cdleme20aN  37605  cdleme20bN  37606  cdleme20l1  37616  cdleme20l2  37617  cdleme22aa  37635  cdleme22a  37636  cdleme22g  37644  cdleme23b  37646  cdleme23c  37647  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme28b  37667  cdleme32b  37738  cdleme32c  37739  cdleme32e  37741  cdleme35h  37752  cdleme35sn2aw  37754  cdleme38m  37759  cdleme40n  37764  cdleme41sn3aw  37770  cdleme41sn4aw  37771  cdlemeg46gfre  37828  cdlemf1  37857  cdlemg1cex  37884  cdlemg2ce  37888  cdlemg4d  37909  cdlemg4  37913  cdlemg7fvN  37920  cdlemg8b  37924  cdlemg8c  37925  cdlemg9a  37928  cdlemg11aq  37934  cdlemg10a  37936  cdlemg12a  37939  cdlemg12b  37940  cdlemg12d  37942  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg13  37948  cdlemg14f  37949  cdlemg14g  37950  cdlemg17b  37958  cdlemg17dN  37959  cdlemg17e  37961  cdlemg17pq  37968  cdlemg17iqN  37970  cdlemg18c  37976  cdlemg18d  37977  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg27a  37988  cdlemg28a  37989  cdlemg31b0N  37990  cdlemg27b  37992  cdlemg31c  37995  cdlemg33b0  37997  cdlemg28  38000  cdlemg33a  38002  cdlemg33  38007  cdlemg35  38009  cdlemg36  38010  cdlemg44a  38027  cdlemg46  38031  cdlemh2  38112  cdlemh  38113  cdlemj1  38117  cdlemk5  38132  cdlemk6  38133  cdlemki  38137  cdlemksv2  38143  cdlemk7  38144  cdlemk11  38145  cdlemkole  38149  cdlemk14  38150  cdlemk16  38153  cdlemk1u  38155  cdlemk18  38164  cdlemk19  38165  cdlemk7u  38166  cdlemk11u  38167  cdlemk33N  38205  cdlemkid2  38220  cdlemkfid3N  38221  cdlemk11ta  38225  cdlemk11tc  38241  cdlemk45  38243  cdlemk46  38244  cdlemk47  38245  cdlemk52  38250  cdlemk53a  38251  cdlemk54  38254  cdlemk55a  38255  cdleml1N  38272  cdleml3N  38274  cdlemn7  38499  cdlemn8  38500  cdlemn10  38502  dihordlem7  38510  dihordlem7b  38511  dihord1  38514  dihord10  38519  dihord11c  38520  dihord2  38523  hlhilphllem  39255  fmuldfeq  42225