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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 1133 . 2 ((𝜒𝜃𝜏) → 𝜏)
213ad2ant3 1130 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  simpl33OLD  1332  simpr33OLD  1350  simp133  1395  simp233  1404  simp333  1413  smogt  7633  bitsfzo  15359  frlmphl  20322  mdetunilem4  20623  mdetuni0  20629  mdetmul  20631  decpmatmullem  20778  logexprlim  25149  ax5seg  26017  iocinioc2  29850  bnj966  31321  eqfunresadj  31966  cgrtr  32405  cgrtr3  32407  ofscom  32420  segconeq  32423  btwnxfr  32469  colinearxfr  32488  fscgr  32493  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem5  32504  btwnconn1lem6  32505  btwnconn1lem8  32507  btwnconn1lem9  32508  btwnconn1lem10  32509  btwnconn1lem11  32510  btwnconn1lem12  32511  brsegle2  32522  seglecgr12im  32523  seglecgr12  32524  segletr  32527  outsideofeq  32543  lshpkrlem5  34904  lshpkrlem6  34905  atbtwnexOLDN  35236  atbtwnex  35237  4noncolr3  35242  3dimlem3a  35249  3dimlem4a  35252  3dim1  35256  3dim2  35257  1cvrat  35265  2atjlej  35268  hlatexch4  35270  ps-2b  35271  2atm  35316  ps-2c  35317  lvolex3N  35327  2atmat  35350  lvolnlelpln  35374  4atlem10  35395  4atlem11b  35397  4atlem11  35398  4at  35402  4at2  35403  2lplnja  35408  2lplnj  35409  dalemclccjdd  35477  paddasslem5  35613  paddasslem15  35623  pmodlem1  35635  dalawlem1  35660  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  dalawlem15  35674  osumcllem5N  35749  osumcllem6N  35750  lhpexle3lem  35800  lhpmcvr4N  35815  lhpmcvr6N  35817  4atexlemex6  35863  4atex2  35866  4atex2-0bOLDN  35868  4atex3  35870  ltrn11at  35936  cdlemd3  35990  cdleme7aa  36032  cdleme7b  36034  cdleme7c  36035  cdleme7d  36036  cdleme7ga  36038  cdleme16aN  36049  cdleme11dN  36052  cdleme11e  36053  cdleme11l  36059  cdleme11  36060  cdleme12  36061  cdleme14  36063  cdleme15c  36066  cdleme16b  36069  cdleme16d  36071  cdleme17b  36077  cdleme17c  36078  cdleme18c  36083  cdleme18d  36085  cdlemeda  36088  cdlemednpq  36089  cdleme19a  36093  cdleme19c  36095  cdleme20aN  36099  cdleme20bN  36100  cdleme20d  36102  cdleme20f  36104  cdleme20g  36105  cdleme20j  36108  cdleme20l1  36110  cdleme21f  36122  cdleme22aa  36129  cdleme22a  36130  cdleme22cN  36132  cdleme22e  36134  cdleme22f2  36137  cdleme22g  36138  cdleme23b  36140  cdleme23c  36141  cdleme26e  36149  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme28a  36160  cdleme28b  36161  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme35h2  36247  cdleme38m  36253  cdleme41sn4aw  36265  cdlemf1  36351  cdlemg1cex  36378  cdlemg2ce  36382  cdlemg4d  36403  cdlemg4f  36405  cdlemg7fvN  36414  cdlemg8a  36417  cdlemg8b  36418  cdlemg8c  36419  cdlemg9a  36422  cdlemg11a  36427  cdlemg11aq  36428  cdlemg10a  36430  cdlemg11b  36432  cdlemg12a  36433  cdlemg12b  36434  cdlemg12d  36436  cdlemg12e  36437  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg14f  36443  cdlemg14g  36444  cdlemg17b  36452  cdlemg17dN  36453  cdlemg17e  36455  cdlemg17h  36458  cdlemg17pq  36462  cdlemg17iqN  36464  cdlemg18b  36469  cdlemg18c  36470  cdlemg18d  36471  cdlemg18  36472  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg31b0N  36484  cdlemg27b  36486  cdlemg33b0  36491  cdlemg33c0  36492  cdlemg28  36494  cdlemg33a  36496  cdlemg35  36503  cdlemg42  36519  cdlemg44a  36521  cdlemg47  36526  cdlemh2  36606  cdlemh  36607  cdlemj1  36611  cdlemk3  36623  cdlemk5  36626  cdlemki  36631  cdlemksv2  36637  cdlemk7  36638  cdlemk11  36639  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk16a  36646  cdlemk16  36647  cdlemkj  36653  cdlemkuv2  36657  cdlemk18  36658  cdlemk19  36659  cdlemk7u  36660  cdlemk12u  36662  cdlemkoatnle-2N  36665  cdlemk13-2N  36666  cdlemkole-2N  36667  cdlemk14-2N  36668  cdlemk15-2N  36669  cdlemk16-2N  36670  cdlemk17-2N  36671  cdlemk18-2N  36676  cdlemk19-2N  36677  cdlemk7u-2N  36678  cdlemk11u-2N  36679  cdlemk12u-2N  36680  cdlemk21-2N  36681  cdlemk20-2N  36682  cdlemk22  36683  cdlemk30  36684  cdlemk31  36686  cdlemk32  36687  cdlemk24-3  36693  cdlemkid2  36714  cdlemkfid3N  36715  cdlemk45  36737  cdlemk46  36738  cdlemk47  36739  cdlemk52  36744  cdlemk53a  36745  cdleml1N  36766  cdleml3N  36768  cdlemn7  36994  cdlemn10  36997  dihordlem7  37005  dihord1  37009  dihord2a  37010  dihord10  37014  dihord11c  37015  dihord2pre2  37017  hlhilphllem  37753  fmuldfeq  40318
  Copyright terms: Public domain W3C validator