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  7635  bitsfzo  15380  frlmphl  20343  mdetunilem4  20644  mdetuni0  20650  mdetmul  20652  decpmatmullem  20799  logexprlim  25171  ax5seg  26039  iocinioc2  29872  bnj966  31343  eqfunresadj  31988  cgrtr  32427  cgrtr3  32429  ofscom  32442  segconeq  32445  btwnxfr  32491  colinearxfr  32510  fscgr  32515  btwnconn1lem1  32522  btwnconn1lem2  32523  btwnconn1lem5  32526  btwnconn1lem6  32527  btwnconn1lem8  32529  btwnconn1lem9  32530  btwnconn1lem10  32531  btwnconn1lem11  32532  btwnconn1lem12  32533  brsegle2  32544  seglecgr12im  32545  seglecgr12  32546  segletr  32549  outsideofeq  32565  lshpkrlem5  34923  lshpkrlem6  34924  atbtwnexOLDN  35255  atbtwnex  35256  4noncolr3  35261  3dimlem3a  35268  3dimlem4a  35271  3dim1  35275  3dim2  35276  1cvrat  35284  2atjlej  35287  hlatexch4  35289  ps-2b  35290  2atm  35335  ps-2c  35336  lvolex3N  35346  2atmat  35369  lvolnlelpln  35393  4atlem10  35414  4atlem11b  35416  4atlem11  35417  4at  35421  4at2  35422  2lplnja  35427  2lplnj  35428  dalemclccjdd  35496  paddasslem5  35632  paddasslem15  35642  pmodlem1  35654  dalawlem1  35679  dalawlem3  35681  dalawlem4  35682  dalawlem5  35683  dalawlem6  35684  dalawlem7  35685  dalawlem8  35686  dalawlem9  35687  dalawlem11  35689  dalawlem12  35690  dalawlem15  35693  osumcllem5N  35768  osumcllem6N  35769  lhpexle3lem  35819  lhpmcvr4N  35834  lhpmcvr6N  35836  4atexlemex6  35882  4atex2  35885  4atex2-0bOLDN  35887  4atex3  35889  ltrn11at  35955  cdlemd3  36009  cdleme7aa  36051  cdleme7b  36053  cdleme7c  36054  cdleme7d  36055  cdleme7ga  36057  cdleme16aN  36068  cdleme11dN  36071  cdleme11e  36072  cdleme11l  36078  cdleme11  36079  cdleme12  36080  cdleme14  36082  cdleme15c  36085  cdleme16b  36088  cdleme16d  36090  cdleme17b  36096  cdleme17c  36097  cdleme18c  36102  cdleme18d  36104  cdlemeda  36107  cdlemednpq  36108  cdleme19a  36112  cdleme19c  36114  cdleme20aN  36118  cdleme20bN  36119  cdleme20d  36121  cdleme20f  36123  cdleme20g  36124  cdleme20j  36127  cdleme20l1  36129  cdleme21f  36141  cdleme22aa  36148  cdleme22a  36149  cdleme22cN  36151  cdleme22e  36153  cdleme22f2  36156  cdleme22g  36157  cdleme23b  36159  cdleme23c  36160  cdleme26e  36168  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme28a  36179  cdleme28b  36180  cdleme32b  36251  cdleme32c  36252  cdleme32e  36254  cdleme35h2  36266  cdleme38m  36272  cdleme41sn4aw  36284  cdlemf1  36370  cdlemg1cex  36397  cdlemg2ce  36401  cdlemg4d  36422  cdlemg4f  36424  cdlemg7fvN  36433  cdlemg8a  36436  cdlemg8b  36437  cdlemg8c  36438  cdlemg9a  36441  cdlemg11a  36446  cdlemg11aq  36447  cdlemg10a  36449  cdlemg11b  36451  cdlemg12a  36452  cdlemg12b  36453  cdlemg12d  36455  cdlemg12e  36456  cdlemg12f  36457  cdlemg12g  36458  cdlemg12  36459  cdlemg13a  36460  cdlemg13  36461  cdlemg14f  36462  cdlemg14g  36463  cdlemg17b  36471  cdlemg17dN  36472  cdlemg17e  36474  cdlemg17h  36477  cdlemg17pq  36481  cdlemg17iqN  36483  cdlemg18b  36488  cdlemg18c  36489  cdlemg18d  36490  cdlemg18  36491  cdlemg19  36493  cdlemg21  36495  cdlemg27a  36501  cdlemg31b0N  36503  cdlemg27b  36505  cdlemg33b0  36510  cdlemg33c0  36511  cdlemg28  36513  cdlemg33a  36515  cdlemg35  36522  cdlemg42  36538  cdlemg44a  36540  cdlemg47  36545  cdlemh2  36625  cdlemh  36626  cdlemj1  36630  cdlemk3  36642  cdlemk5  36645  cdlemki  36650  cdlemksv2  36656  cdlemk7  36657  cdlemk11  36658  cdlemk12  36659  cdlemkole  36662  cdlemk14  36663  cdlemk15  36664  cdlemk16a  36665  cdlemk16  36666  cdlemkj  36672  cdlemkuv2  36676  cdlemk18  36677  cdlemk19  36678  cdlemk7u  36679  cdlemk12u  36681  cdlemkoatnle-2N  36684  cdlemk13-2N  36685  cdlemkole-2N  36686  cdlemk14-2N  36687  cdlemk15-2N  36688  cdlemk16-2N  36689  cdlemk17-2N  36690  cdlemk18-2N  36695  cdlemk19-2N  36696  cdlemk7u-2N  36697  cdlemk11u-2N  36698  cdlemk12u-2N  36699  cdlemk21-2N  36700  cdlemk20-2N  36701  cdlemk22  36702  cdlemk30  36703  cdlemk31  36705  cdlemk32  36706  cdlemk24-3  36712  cdlemkid2  36733  cdlemkfid3N  36734  cdlemk45  36756  cdlemk46  36757  cdlemk47  36758  cdlemk52  36763  cdlemk53a  36764  cdleml1N  36785  cdleml3N  36787  cdlemn7  37013  cdlemn10  37016  dihordlem7  37024  dihord1  37028  dihord2a  37029  dihord10  37033  dihord11c  37034  dihord2pre2  37036  hlhilphllem  37772  fmuldfeq  40337
  Copyright terms: Public domain W3C validator