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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 1061 . 2 ((𝜒𝜃𝜏) → 𝜏)
213ad2ant3 1082 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simpl33  1142  simpr33  1151  simp133  1196  simp233  1205  simp333  1214  smogt  7409  bitsfzo  15081  frlmphl  20039  mdetunilem4  20340  mdetuni0  20346  mdetmul  20348  decpmatmullem  20495  logexprlim  24850  ax5seg  25718  iocinioc2  29385  bnj966  30722  cgrtr  31741  cgrtr3  31743  ofscom  31756  segconeq  31759  btwnxfr  31805  colinearxfr  31824  fscgr  31829  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem8  31843  btwnconn1lem9  31844  btwnconn1lem10  31845  btwnconn1lem11  31846  btwnconn1lem12  31847  brsegle2  31858  seglecgr12im  31859  seglecgr12  31860  segletr  31863  outsideofeq  31879  lshpkrlem5  33881  lshpkrlem6  33882  atbtwnexOLDN  34213  atbtwnex  34214  4noncolr3  34219  3dimlem3a  34226  3dimlem4a  34229  3dim1  34233  3dim2  34234  1cvrat  34242  2atjlej  34245  hlatexch4  34247  ps-2b  34248  2atm  34293  ps-2c  34294  lvolex3N  34304  2atmat  34327  lvolnlelpln  34351  4atlem10  34372  4atlem11b  34374  4atlem11  34375  4at  34379  4at2  34380  2lplnja  34385  2lplnj  34386  dalemclccjdd  34454  paddasslem5  34590  paddasslem15  34600  pmodlem1  34612  dalawlem1  34637  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem12  34648  dalawlem15  34651  osumcllem5N  34726  osumcllem6N  34727  lhpexle3lem  34777  lhpmcvr4N  34792  lhpmcvr6N  34794  4atexlemex6  34840  4atex2  34843  4atex2-0bOLDN  34845  4atex3  34847  ltrn11at  34913  cdlemd3  34967  cdleme7aa  35009  cdleme7b  35011  cdleme7c  35012  cdleme7d  35013  cdleme7ga  35015  cdleme16aN  35026  cdleme11dN  35029  cdleme11e  35030  cdleme11l  35036  cdleme11  35037  cdleme12  35038  cdleme14  35040  cdleme15c  35043  cdleme16b  35046  cdleme16d  35048  cdleme17b  35054  cdleme17c  35055  cdleme18c  35060  cdleme18d  35062  cdlemeda  35065  cdlemednpq  35066  cdleme19a  35071  cdleme19c  35073  cdleme20aN  35077  cdleme20bN  35078  cdleme20d  35080  cdleme20f  35082  cdleme20g  35083  cdleme20j  35086  cdleme20l1  35088  cdleme21f  35100  cdleme22aa  35107  cdleme22a  35108  cdleme22cN  35110  cdleme22e  35112  cdleme22f2  35115  cdleme22g  35116  cdleme23b  35118  cdleme23c  35119  cdleme26e  35127  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme28a  35138  cdleme28b  35139  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35h2  35225  cdleme38m  35231  cdleme41sn4aw  35243  cdlemf1  35329  cdlemg1cex  35356  cdlemg2ce  35360  cdlemg4d  35381  cdlemg4f  35383  cdlemg7fvN  35392  cdlemg8a  35395  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg11a  35405  cdlemg11aq  35406  cdlemg10a  35408  cdlemg11b  35410  cdlemg12a  35411  cdlemg12b  35412  cdlemg12d  35414  cdlemg12e  35415  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg14f  35421  cdlemg14g  35422  cdlemg17b  35430  cdlemg17dN  35431  cdlemg17e  35433  cdlemg17h  35436  cdlemg17pq  35440  cdlemg17iqN  35442  cdlemg18b  35447  cdlemg18c  35448  cdlemg18d  35449  cdlemg18  35450  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg31b0N  35462  cdlemg27b  35464  cdlemg33b0  35469  cdlemg33c0  35470  cdlemg28  35472  cdlemg33a  35474  cdlemg35  35481  cdlemg42  35497  cdlemg44a  35499  cdlemg47  35504  cdlemh2  35584  cdlemh  35585  cdlemj1  35589  cdlemk3  35601  cdlemk5  35604  cdlemki  35609  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemkj  35631  cdlemkuv2  35635  cdlemk18  35636  cdlemk19  35637  cdlemk7u  35638  cdlemk12u  35640  cdlemkoatnle-2N  35643  cdlemk13-2N  35644  cdlemkole-2N  35645  cdlemk14-2N  35646  cdlemk15-2N  35647  cdlemk16-2N  35648  cdlemk17-2N  35649  cdlemk18-2N  35654  cdlemk19-2N  35655  cdlemk7u-2N  35656  cdlemk11u-2N  35657  cdlemk12u-2N  35658  cdlemk21-2N  35659  cdlemk20-2N  35660  cdlemk22  35661  cdlemk30  35662  cdlemk31  35664  cdlemk32  35665  cdlemk24-3  35671  cdlemkid2  35692  cdlemkfid3N  35693  cdlemk45  35715  cdlemk46  35716  cdlemk47  35717  cdlemk52  35722  cdlemk53a  35723  cdleml1N  35744  cdleml3N  35746  cdlemn7  35972  cdlemn10  35975  dihordlem7  35983  dihord1  35987  dihord2a  35988  dihord10  35992  dihord11c  35993  dihord2pre2  35995  hlhilphllem  36731  fmuldfeq  39219
  Copyright terms: Public domain W3C validator