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  7993  bitsfzo  15772  frlmphl  20853  mdetunilem4  21152  mdetuni0  21158  mdetmul  21160  decpmatmullem  21307  logexprlim  25728  ax5seg  26651  iocinioc2  30428  bnj966  32115  eqfunresadj  32901  cgrtr  33350  cgrtr3  33352  ofscom  33365  segconeq  33368  btwnxfr  33414  colinearxfr  33433  fscgr  33438  btwnconn1lem1  33445  btwnconn1lem2  33446  btwnconn1lem5  33449  btwnconn1lem6  33450  btwnconn1lem8  33452  btwnconn1lem9  33453  btwnconn1lem10  33454  btwnconn1lem11  33455  btwnconn1lem12  33456  brsegle2  33467  seglecgr12im  33468  seglecgr12  33469  segletr  33472  outsideofeq  33488  lshpkrlem5  36130  lshpkrlem6  36131  atbtwnexOLDN  36463  atbtwnex  36464  4noncolr3  36469  3dimlem3a  36476  3dimlem4a  36479  3dim1  36483  3dim2  36484  1cvrat  36492  2atjlej  36495  hlatexch4  36497  ps-2b  36498  2atm  36543  ps-2c  36544  lvolex3N  36554  2atmat  36577  lvolnlelpln  36601  4atlem10  36622  4atlem11b  36624  4atlem11  36625  4at  36629  4at2  36630  2lplnja  36635  2lplnj  36636  dalemclccjdd  36704  paddasslem5  36840  paddasslem15  36850  pmodlem1  36862  dalawlem1  36887  dalawlem3  36889  dalawlem4  36890  dalawlem5  36891  dalawlem6  36892  dalawlem7  36893  dalawlem8  36894  dalawlem9  36895  dalawlem11  36897  dalawlem12  36898  dalawlem15  36901  osumcllem5N  36976  osumcllem6N  36977  lhpexle3lem  37027  lhpmcvr4N  37042  lhpmcvr6N  37044  4atexlemex6  37090  4atex2  37093  4atex2-0bOLDN  37095  4atex3  37097  ltrn11at  37163  cdlemd3  37216  cdleme7aa  37258  cdleme7b  37260  cdleme7c  37261  cdleme7d  37262  cdleme7ga  37264  cdleme16aN  37275  cdleme11dN  37278  cdleme11e  37279  cdleme11l  37285  cdleme11  37286  cdleme12  37287  cdleme14  37289  cdleme15c  37292  cdleme16b  37295  cdleme16d  37297  cdleme17b  37303  cdleme17c  37304  cdleme18c  37309  cdleme18d  37311  cdlemeda  37314  cdlemednpq  37315  cdleme19a  37319  cdleme19c  37321  cdleme20aN  37325  cdleme20bN  37326  cdleme20d  37328  cdleme20f  37330  cdleme20g  37331  cdleme20j  37334  cdleme20l1  37336  cdleme21f  37348  cdleme22aa  37355  cdleme22a  37356  cdleme22cN  37358  cdleme22e  37360  cdleme22f2  37363  cdleme22g  37364  cdleme23b  37366  cdleme23c  37367  cdleme26e  37375  cdleme26fALTN  37378  cdleme26f  37379  cdleme26f2ALTN  37380  cdleme26f2  37381  cdleme28a  37386  cdleme28b  37387  cdleme32b  37458  cdleme32c  37459  cdleme32e  37461  cdleme35h2  37473  cdleme38m  37479  cdleme41sn4aw  37491  cdlemf1  37577  cdlemg1cex  37604  cdlemg2ce  37608  cdlemg4d  37629  cdlemg4f  37631  cdlemg7fvN  37640  cdlemg8a  37643  cdlemg8b  37644  cdlemg8c  37645  cdlemg9a  37648  cdlemg11a  37653  cdlemg11aq  37654  cdlemg10a  37656  cdlemg11b  37658  cdlemg12a  37659  cdlemg12b  37660  cdlemg12d  37662  cdlemg12e  37663  cdlemg12f  37664  cdlemg12g  37665  cdlemg12  37666  cdlemg13a  37667  cdlemg13  37668  cdlemg14f  37669  cdlemg14g  37670  cdlemg17b  37678  cdlemg17dN  37679  cdlemg17e  37681  cdlemg17h  37684  cdlemg17pq  37688  cdlemg17iqN  37690  cdlemg18b  37695  cdlemg18c  37696  cdlemg18d  37697  cdlemg18  37698  cdlemg19  37700  cdlemg21  37702  cdlemg27a  37708  cdlemg31b0N  37710  cdlemg27b  37712  cdlemg33b0  37717  cdlemg33c0  37718  cdlemg28  37720  cdlemg33a  37722  cdlemg35  37729  cdlemg42  37745  cdlemg44a  37747  cdlemg47  37752  cdlemh2  37832  cdlemh  37833  cdlemj1  37837  cdlemk3  37849  cdlemk5  37852  cdlemki  37857  cdlemksv2  37863  cdlemk7  37864  cdlemk11  37865  cdlemk12  37866  cdlemkole  37869  cdlemk14  37870  cdlemk15  37871  cdlemk16a  37872  cdlemk16  37873  cdlemkj  37879  cdlemkuv2  37883  cdlemk18  37884  cdlemk19  37885  cdlemk7u  37886  cdlemk12u  37888  cdlemkoatnle-2N  37891  cdlemk13-2N  37892  cdlemkole-2N  37893  cdlemk14-2N  37894  cdlemk15-2N  37895  cdlemk16-2N  37896  cdlemk17-2N  37897  cdlemk18-2N  37902  cdlemk19-2N  37903  cdlemk7u-2N  37904  cdlemk11u-2N  37905  cdlemk12u-2N  37906  cdlemk21-2N  37907  cdlemk20-2N  37908  cdlemk22  37909  cdlemk30  37910  cdlemk31  37912  cdlemk32  37913  cdlemk24-3  37919  cdlemkid2  37940  cdlemkfid3N  37941  cdlemk45  37963  cdlemk46  37964  cdlemk47  37965  cdlemk52  37970  cdlemk53a  37971  cdleml1N  37992  cdleml3N  37994  cdlemn7  38219  cdlemn10  38222  dihordlem7  38230  dihord1  38234  dihord2a  38235  dihord10  38239  dihord11c  38240  dihord2pre2  38242  hlhilphllem  38975  fmuldfeq  41740
  Copyright terms: Public domain W3C validator