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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 1056 . 2 ((𝜒𝜃𝜏) → 𝜏)
213ad2ant3 1077 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  simpl33  1137  simpr33  1146  simp133  1191  simp233  1200  simp333  1209  smogt  7351  bitsfzo  14995  frlmphl  19939  mdetunilem4  20240  mdetuni0  20246  mdetmul  20248  decpmatmullem  20395  logexprlim  24750  ax5seg  25618  iocinioc2  28931  bnj966  30268  cgrtr  31269  cgrtr3  31271  ofscom  31284  segconeq  31287  btwnxfr  31333  colinearxfr  31352  fscgr  31357  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem12  31375  brsegle2  31386  seglecgr12im  31387  seglecgr12  31388  segletr  31391  outsideofeq  31407  lshpkrlem5  33419  lshpkrlem6  33420  atbtwnexOLDN  33751  atbtwnex  33752  4noncolr3  33757  3dimlem3a  33764  3dimlem4a  33767  3dim1  33771  3dim2  33772  1cvrat  33780  2atjlej  33783  hlatexch4  33785  ps-2b  33786  2atm  33831  ps-2c  33832  lvolex3N  33842  2atmat  33865  lvolnlelpln  33889  4atlem10  33910  4atlem11b  33912  4atlem11  33913  4at  33917  4at2  33918  2lplnja  33923  2lplnj  33924  dalemclccjdd  33992  paddasslem5  34128  paddasslem15  34138  pmodlem1  34150  dalawlem1  34175  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  osumcllem5N  34264  osumcllem6N  34265  lhpexle3lem  34315  lhpmcvr4N  34330  lhpmcvr6N  34332  4atexlemex6  34378  4atex2  34381  4atex2-0bOLDN  34383  4atex3  34385  ltrn11at  34451  cdlemd3  34505  cdleme7aa  34547  cdleme7b  34549  cdleme7c  34550  cdleme7d  34551  cdleme7ga  34553  cdleme16aN  34564  cdleme11dN  34567  cdleme11e  34568  cdleme11l  34574  cdleme11  34575  cdleme12  34576  cdleme14  34578  cdleme15c  34581  cdleme16b  34584  cdleme16d  34586  cdleme17b  34592  cdleme17c  34593  cdleme18c  34598  cdleme18d  34600  cdlemeda  34603  cdlemednpq  34604  cdleme19a  34609  cdleme19c  34611  cdleme20aN  34615  cdleme20bN  34616  cdleme20d  34618  cdleme20f  34620  cdleme20g  34621  cdleme20j  34624  cdleme20l1  34626  cdleme21f  34638  cdleme22aa  34645  cdleme22a  34646  cdleme22cN  34648  cdleme22e  34650  cdleme22f2  34653  cdleme22g  34654  cdleme23b  34656  cdleme23c  34657  cdleme26e  34665  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme28a  34676  cdleme28b  34677  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35h2  34763  cdleme38m  34769  cdleme41sn4aw  34781  cdlemf1  34867  cdlemg1cex  34894  cdlemg2ce  34898  cdlemg4d  34919  cdlemg4f  34921  cdlemg7fvN  34930  cdlemg8a  34933  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg11a  34943  cdlemg11aq  34944  cdlemg10a  34946  cdlemg11b  34948  cdlemg12a  34949  cdlemg12b  34950  cdlemg12d  34952  cdlemg12e  34953  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17b  34968  cdlemg17dN  34969  cdlemg17e  34971  cdlemg17h  34974  cdlemg17pq  34978  cdlemg17iqN  34980  cdlemg18b  34985  cdlemg18c  34986  cdlemg18d  34987  cdlemg18  34988  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg31b0N  35000  cdlemg27b  35002  cdlemg33b0  35007  cdlemg33c0  35008  cdlemg28  35010  cdlemg33a  35012  cdlemg35  35019  cdlemg42  35035  cdlemg44a  35037  cdlemg47  35042  cdlemh2  35122  cdlemh  35123  cdlemj1  35127  cdlemk3  35139  cdlemk5  35142  cdlemki  35147  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk16a  35162  cdlemk16  35163  cdlemkj  35169  cdlemkuv2  35173  cdlemk18  35174  cdlemk19  35175  cdlemk7u  35176  cdlemk12u  35178  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk21-2N  35197  cdlemk20-2N  35198  cdlemk22  35199  cdlemk30  35200  cdlemk31  35202  cdlemk32  35203  cdlemk24-3  35209  cdlemkid2  35230  cdlemkfid3N  35231  cdlemk45  35253  cdlemk46  35254  cdlemk47  35255  cdlemk52  35260  cdlemk53a  35261  cdleml1N  35282  cdleml3N  35284  cdlemn7  35510  cdlemn10  35513  dihordlem7  35521  dihord1  35525  dihord2a  35526  dihord10  35530  dihord11c  35531  dihord2pre2  35533  hlhilphllem  36269  fmuldfeq  38650
  Copyright terms: Public domain W3C validator