MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp33 Structured version   Visualization version   GIF version

Theorem simp33 1208
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp33 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)

Proof of Theorem simp33
StepHypRef Expression
1 simp3 1135 . 2 ((𝜒𝜃𝜏) → 𝜏)
213ad2ant3 1132 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)
Colors of variables: wff setvar class
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  7991  bitsfzo  15773  frlmphl  20468  mdetunilem4  21218  mdetuni0  21224  mdetmul  21226  decpmatmullem  21374  logexprlim  25807  ax5seg  26730  iocinioc2  30512  bnj966  32290  eqfunresadj  33078  cgrtr  33527  cgrtr3  33529  ofscom  33542  segconeq  33545  btwnxfr  33591  colinearxfr  33610  fscgr  33615  btwnconn1lem1  33622  btwnconn1lem2  33623  btwnconn1lem5  33626  btwnconn1lem6  33627  btwnconn1lem8  33629  btwnconn1lem9  33630  btwnconn1lem10  33631  btwnconn1lem11  33632  btwnconn1lem12  33633  brsegle2  33644  seglecgr12im  33645  seglecgr12  33646  segletr  33649  outsideofeq  33665  lshpkrlem5  36369  lshpkrlem6  36370  atbtwnexOLDN  36702  atbtwnex  36703  4noncolr3  36708  3dimlem3a  36715  3dimlem4a  36718  3dim1  36722  3dim2  36723  1cvrat  36731  2atjlej  36734  hlatexch4  36736  ps-2b  36737  2atm  36782  ps-2c  36783  lvolex3N  36793  2atmat  36816  lvolnlelpln  36840  4atlem10  36861  4atlem11b  36863  4atlem11  36864  4at  36868  4at2  36869  2lplnja  36874  2lplnj  36875  dalemclccjdd  36943  paddasslem5  37079  paddasslem15  37089  pmodlem1  37101  dalawlem1  37126  dalawlem3  37128  dalawlem4  37129  dalawlem5  37130  dalawlem6  37131  dalawlem7  37132  dalawlem8  37133  dalawlem9  37134  dalawlem11  37136  dalawlem12  37137  dalawlem15  37140  osumcllem5N  37215  osumcllem6N  37216  lhpexle3lem  37266  lhpmcvr4N  37281  lhpmcvr6N  37283  4atexlemex6  37329  4atex2  37332  4atex2-0bOLDN  37334  4atex3  37336  ltrn11at  37402  cdlemd3  37455  cdleme7aa  37497  cdleme7b  37499  cdleme7c  37500  cdleme7d  37501  cdleme7ga  37503  cdleme16aN  37514  cdleme11dN  37517  cdleme11e  37518  cdleme11l  37524  cdleme11  37525  cdleme12  37526  cdleme14  37528  cdleme15c  37531  cdleme16b  37534  cdleme16d  37536  cdleme17b  37542  cdleme17c  37543  cdleme18c  37548  cdleme18d  37550  cdlemeda  37553  cdlemednpq  37554  cdleme19a  37558  cdleme19c  37560  cdleme20aN  37564  cdleme20bN  37565  cdleme20d  37567  cdleme20f  37569  cdleme20g  37570  cdleme20j  37573  cdleme20l1  37575  cdleme21f  37587  cdleme22aa  37594  cdleme22a  37595  cdleme22cN  37597  cdleme22e  37599  cdleme22f2  37602  cdleme22g  37603  cdleme23b  37605  cdleme23c  37606  cdleme26e  37614  cdleme26fALTN  37617  cdleme26f  37618  cdleme26f2ALTN  37619  cdleme26f2  37620  cdleme28a  37625  cdleme28b  37626  cdleme32b  37697  cdleme32c  37698  cdleme32e  37700  cdleme35h2  37712  cdleme38m  37718  cdleme41sn4aw  37730  cdlemf1  37816  cdlemg1cex  37843  cdlemg2ce  37847  cdlemg4d  37868  cdlemg4f  37870  cdlemg7fvN  37879  cdlemg8a  37882  cdlemg8b  37883  cdlemg8c  37884  cdlemg9a  37887  cdlemg11a  37892  cdlemg11aq  37893  cdlemg10a  37895  cdlemg11b  37897  cdlemg12a  37898  cdlemg12b  37899  cdlemg12d  37901  cdlemg12e  37902  cdlemg12f  37903  cdlemg12g  37904  cdlemg12  37905  cdlemg13a  37906  cdlemg13  37907  cdlemg14f  37908  cdlemg14g  37909  cdlemg17b  37917  cdlemg17dN  37918  cdlemg17e  37920  cdlemg17h  37923  cdlemg17pq  37927  cdlemg17iqN  37929  cdlemg18b  37934  cdlemg18c  37935  cdlemg18d  37936  cdlemg18  37937  cdlemg19  37939  cdlemg21  37941  cdlemg27a  37947  cdlemg31b0N  37949  cdlemg27b  37951  cdlemg33b0  37956  cdlemg33c0  37957  cdlemg28  37959  cdlemg33a  37961  cdlemg35  37968  cdlemg42  37984  cdlemg44a  37986  cdlemg47  37991  cdlemh2  38071  cdlemh  38072  cdlemj1  38076  cdlemk3  38088  cdlemk5  38091  cdlemki  38096  cdlemksv2  38102  cdlemk7  38103  cdlemk11  38104  cdlemk12  38105  cdlemkole  38108  cdlemk14  38109  cdlemk15  38110  cdlemk16a  38111  cdlemk16  38112  cdlemkj  38118  cdlemkuv2  38122  cdlemk18  38123  cdlemk19  38124  cdlemk7u  38125  cdlemk12u  38127  cdlemkoatnle-2N  38130  cdlemk13-2N  38131  cdlemkole-2N  38132  cdlemk14-2N  38133  cdlemk15-2N  38134  cdlemk16-2N  38135  cdlemk17-2N  38136  cdlemk18-2N  38141  cdlemk19-2N  38142  cdlemk7u-2N  38143  cdlemk11u-2N  38144  cdlemk12u-2N  38145  cdlemk21-2N  38146  cdlemk20-2N  38147  cdlemk22  38148  cdlemk30  38149  cdlemk31  38151  cdlemk32  38152  cdlemk24-3  38158  cdlemkid2  38179  cdlemkfid3N  38180  cdlemk45  38202  cdlemk46  38203  cdlemk47  38204  cdlemk52  38209  cdlemk53a  38210  cdleml1N  38231  cdleml3N  38233  cdlemn7  38458  cdlemn10  38461  dihordlem7  38469  dihord1  38473  dihord2a  38474  dihord10  38478  dihord11c  38479  dihord2pre2  38481  hlhilphllem  39214  fmuldfeq  42165
  Copyright terms: Public domain W3C validator