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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 1130 . 2 ((𝜒𝜃𝜏) → 𝜏)
213ad2ant3 1127 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp133  1302  simp233  1311  simp333  1320  smogt  7995  bitsfzo  15774  frlmphl  20855  mdetunilem4  21154  mdetuni0  21160  mdetmul  21162  decpmatmullem  21309  logexprlim  25729  ax5seg  26652  iocinioc2  30429  bnj966  32116  eqfunresadj  32902  cgrtr  33351  cgrtr3  33353  ofscom  33366  segconeq  33369  btwnxfr  33415  colinearxfr  33434  fscgr  33439  btwnconn1lem1  33446  btwnconn1lem2  33447  btwnconn1lem5  33450  btwnconn1lem6  33451  btwnconn1lem8  33453  btwnconn1lem9  33454  btwnconn1lem10  33455  btwnconn1lem11  33456  btwnconn1lem12  33457  brsegle2  33468  seglecgr12im  33469  seglecgr12  33470  segletr  33473  outsideofeq  33489  lshpkrlem5  36132  lshpkrlem6  36133  atbtwnexOLDN  36465  atbtwnex  36466  4noncolr3  36471  3dimlem3a  36478  3dimlem4a  36481  3dim1  36485  3dim2  36486  1cvrat  36494  2atjlej  36497  hlatexch4  36499  ps-2b  36500  2atm  36545  ps-2c  36546  lvolex3N  36556  2atmat  36579  lvolnlelpln  36603  4atlem10  36624  4atlem11b  36626  4atlem11  36627  4at  36631  4at2  36632  2lplnja  36637  2lplnj  36638  dalemclccjdd  36706  paddasslem5  36842  paddasslem15  36852  pmodlem1  36864  dalawlem1  36889  dalawlem3  36891  dalawlem4  36892  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem8  36896  dalawlem9  36897  dalawlem11  36899  dalawlem12  36900  dalawlem15  36903  osumcllem5N  36978  osumcllem6N  36979  lhpexle3lem  37029  lhpmcvr4N  37044  lhpmcvr6N  37046  4atexlemex6  37092  4atex2  37095  4atex2-0bOLDN  37097  4atex3  37099  ltrn11at  37165  cdlemd3  37218  cdleme7aa  37260  cdleme7b  37262  cdleme7c  37263  cdleme7d  37264  cdleme7ga  37266  cdleme16aN  37277  cdleme11dN  37280  cdleme11e  37281  cdleme11l  37287  cdleme11  37288  cdleme12  37289  cdleme14  37291  cdleme15c  37294  cdleme16b  37297  cdleme16d  37299  cdleme17b  37305  cdleme17c  37306  cdleme18c  37311  cdleme18d  37313  cdlemeda  37316  cdlemednpq  37317  cdleme19a  37321  cdleme19c  37323  cdleme20aN  37327  cdleme20bN  37328  cdleme20d  37330  cdleme20f  37332  cdleme20g  37333  cdleme20j  37336  cdleme20l1  37338  cdleme21f  37350  cdleme22aa  37357  cdleme22a  37358  cdleme22cN  37360  cdleme22e  37362  cdleme22f2  37365  cdleme22g  37366  cdleme23b  37368  cdleme23c  37369  cdleme26e  37377  cdleme26fALTN  37380  cdleme26f  37381  cdleme26f2ALTN  37382  cdleme26f2  37383  cdleme28a  37388  cdleme28b  37389  cdleme32b  37460  cdleme32c  37461  cdleme32e  37463  cdleme35h2  37475  cdleme38m  37481  cdleme41sn4aw  37493  cdlemf1  37579  cdlemg1cex  37606  cdlemg2ce  37610  cdlemg4d  37631  cdlemg4f  37633  cdlemg7fvN  37642  cdlemg8a  37645  cdlemg8b  37646  cdlemg8c  37647  cdlemg9a  37650  cdlemg11a  37655  cdlemg11aq  37656  cdlemg10a  37658  cdlemg11b  37660  cdlemg12a  37661  cdlemg12b  37662  cdlemg12d  37664  cdlemg12e  37665  cdlemg12f  37666  cdlemg12g  37667  cdlemg12  37668  cdlemg13a  37669  cdlemg13  37670  cdlemg14f  37671  cdlemg14g  37672  cdlemg17b  37680  cdlemg17dN  37681  cdlemg17e  37683  cdlemg17h  37686  cdlemg17pq  37690  cdlemg17iqN  37692  cdlemg18b  37697  cdlemg18c  37698  cdlemg18d  37699  cdlemg18  37700  cdlemg19  37702  cdlemg21  37704  cdlemg27a  37710  cdlemg31b0N  37712  cdlemg27b  37714  cdlemg33b0  37719  cdlemg33c0  37720  cdlemg28  37722  cdlemg33a  37724  cdlemg35  37731  cdlemg42  37747  cdlemg44a  37749  cdlemg47  37754  cdlemh2  37834  cdlemh  37835  cdlemj1  37839  cdlemk3  37851  cdlemk5  37854  cdlemki  37859  cdlemksv2  37865  cdlemk7  37866  cdlemk11  37867  cdlemk12  37868  cdlemkole  37871  cdlemk14  37872  cdlemk15  37873  cdlemk16a  37874  cdlemk16  37875  cdlemkj  37881  cdlemkuv2  37885  cdlemk18  37886  cdlemk19  37887  cdlemk7u  37888  cdlemk12u  37890  cdlemkoatnle-2N  37893  cdlemk13-2N  37894  cdlemkole-2N  37895  cdlemk14-2N  37896  cdlemk15-2N  37897  cdlemk16-2N  37898  cdlemk17-2N  37899  cdlemk18-2N  37904  cdlemk19-2N  37905  cdlemk7u-2N  37906  cdlemk11u-2N  37907  cdlemk12u-2N  37908  cdlemk21-2N  37909  cdlemk20-2N  37910  cdlemk22  37911  cdlemk30  37912  cdlemk31  37914  cdlemk32  37915  cdlemk24-3  37921  cdlemkid2  37942  cdlemkfid3N  37943  cdlemk45  37965  cdlemk46  37966  cdlemk47  37967  cdlemk52  37972  cdlemk53a  37973  cdleml1N  37994  cdleml3N  37996  cdlemn7  38221  cdlemn10  38224  dihordlem7  38232  dihord1  38236  dihord2a  38237  dihord10  38241  dihord11c  38242  dihord2pre2  38244  hlhilphllem  38977  fmuldfeq  41744
  Copyright terms: Public domain W3C validator