Theorem simp33 1208

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 1135	. 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:  simp133  1307  simp233  1316  simp333  1325  smogt  7987  bitsfzo  15774  frlmphl  20470  mdetunilem4  21220  mdetuni0  21226  mdetmul  21228  decpmatmullem  21376  logexprlim  25809  ax5seg  26732  iocinioc2  30528  bnj966  32326  eqfunresadj  33117  cgrtr  33566  cgrtr3  33568  ofscom  33581  segconeq  33584  btwnxfr  33630  colinearxfr  33649  fscgr  33654  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem8  33668  btwnconn1lem9  33669  btwnconn1lem10  33670  btwnconn1lem11  33671  btwnconn1lem12  33672  brsegle2  33683  seglecgr12im  33684  seglecgr12  33685  segletr  33688  outsideofeq  33704  lshpkrlem5  36410  lshpkrlem6  36411  atbtwnexOLDN  36743  atbtwnex  36744  4noncolr3  36749  3dimlem3a  36756  3dimlem4a  36759  3dim1  36763  3dim2  36764  1cvrat  36772  2atjlej  36775  hlatexch4  36777  ps-2b  36778  2atm  36823  ps-2c  36824  lvolex3N  36834  2atmat  36857  lvolnlelpln  36881  4atlem10  36902  4atlem11b  36904  4atlem11  36905  4at  36909  4at2  36910  2lplnja  36915  2lplnj  36916  dalemclccjdd  36984  paddasslem5  37120  paddasslem15  37130  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  4atex3  37377  ltrn11at  37443  cdlemd3  37496  cdleme7aa  37538  cdleme7b  37540  cdleme7c  37541  cdleme7d  37542  cdleme7ga  37544  cdleme16aN  37555  cdleme11dN  37558  cdleme11e  37559  cdleme11l  37565  cdleme11  37566  cdleme12  37567  cdleme14  37569  cdleme15c  37572  cdleme16b  37575  cdleme16d  37577  cdleme17b  37583  cdleme17c  37584  cdleme18c  37589  cdleme18d  37591  cdlemeda  37594  cdlemednpq  37595  cdleme19a  37599  cdleme19c  37601  cdleme20aN  37605  cdleme20bN  37606  cdleme20d  37608  cdleme20f  37610  cdleme20g  37611  cdleme20j  37614  cdleme20l1  37616  cdleme21f  37628  cdleme22aa  37635  cdleme22a  37636  cdleme22cN  37638  cdleme22e  37640  cdleme22f2  37643  cdleme22g  37644  cdleme23b  37646  cdleme23c  37647  cdleme26e  37655  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme28a  37666  cdleme28b  37667  cdleme32b  37738  cdleme32c  37739  cdleme32e  37741  cdleme35h2  37753  cdleme38m  37759  cdleme41sn4aw  37771  cdlemf1  37857  cdlemg1cex  37884  cdlemg2ce  37888  cdlemg4d  37909  cdlemg4f  37911  cdlemg7fvN  37920  cdlemg8a  37923  cdlemg8b  37924  cdlemg8c  37925  cdlemg9a  37928  cdlemg11a  37933  cdlemg11aq  37934  cdlemg10a  37936  cdlemg11b  37938  cdlemg12a  37939  cdlemg12b  37940  cdlemg12d  37942  cdlemg12e  37943  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg13  37948  cdlemg14f  37949  cdlemg14g  37950  cdlemg17b  37958  cdlemg17dN  37959  cdlemg17e  37961  cdlemg17h  37964  cdlemg17pq  37968  cdlemg17iqN  37970  cdlemg18b  37975  cdlemg18c  37976  cdlemg18d  37977  cdlemg18  37978  cdlemg19  37980  cdlemg21  37982  cdlemg27a  37988  cdlemg31b0N  37990  cdlemg27b  37992  cdlemg33b0  37997  cdlemg33c0  37998  cdlemg28  38000  cdlemg33a  38002  cdlemg35  38009  cdlemg42  38025  cdlemg44a  38027  cdlemg47  38032  cdlemh2  38112  cdlemh  38113  cdlemj1  38117  cdlemk3  38129  cdlemk5  38132  cdlemki  38137  cdlemksv2  38143  cdlemk7  38144  cdlemk11  38145  cdlemk12  38146  cdlemkole  38149  cdlemk14  38150  cdlemk15  38151  cdlemk16a  38152  cdlemk16  38153  cdlemkj  38159  cdlemkuv2  38163  cdlemk18  38164  cdlemk19  38165  cdlemk7u  38166  cdlemk12u  38168  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk7u-2N  38184  cdlemk11u-2N  38185  cdlemk12u-2N  38186  cdlemk21-2N  38187  cdlemk20-2N  38188  cdlemk22  38189  cdlemk30  38190  cdlemk31  38192  cdlemk32  38193  cdlemk24-3  38199  cdlemkid2  38220  cdlemkfid3N  38221  cdlemk45  38243  cdlemk46  38244  cdlemk47  38245  cdlemk52  38250  cdlemk53a  38251  cdleml1N  38272  cdleml3N  38274  cdlemn7  38499  cdlemn10  38502  dihordlem7  38510  dihord1  38514  dihord2a  38515  dihord10  38519  dihord11c  38520  dihord2pre2  38522  hlhilphllem  39255  fmuldfeq  42225