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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 1060 . 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:  simpl32  1141  simpr32  1150  simp132  1195  simp232  1204  simp332  1213  smogt  7409  axdc3lem4  9219  bitsfzo  15081  frlmphl  20039  mdetunilem4  20340  mdetuni0  20346  mdetmul  20348  decpmatmullem  20495  logfacbnd3  24848  logexprlim  24850  log2sumbnd  25133  ax5seg  25718  iocinioc2  29385  totprob  30270  nosires  31577  cgrtr  31741  cgrtr3  31743  ofscom  31756  cgrextend  31757  segconeq  31759  ifscgr  31793  colinearxfr  31824  brofs2  31826  brifs2  31827  fscgr  31829  btwnconn1lem2  31837  btwnconn1lem9  31844  btwnconn1lem10  31845  btwnconn1lem11  31846  btwnconn1lem12  31847  brsegle2  31858  seglecgr12im  31859  seglecgr12  31860  segletr  31863  outsideofeq  31879  ivthALT  31972  lshpkrlem5  33881  lshpkrlem6  33882  atbtwnexOLDN  34213  atbtwnex  34214  4noncolr3  34219  3dimlem3a  34226  3dim1  34233  3dim2  34234  1cvrat  34242  2atjlej  34245  hlatexch4  34247  ps-2b  34248  2atm  34293  ps-2c  34294  2atmat  34327  4atlem10  34372  4atlem11b  34374  4atlem11  34375  4at  34379  4at2  34380  2lplnja  34385  2lplnj  34386  dalemswapyz  34422  dalem-ddly  34452  cdlemb  34560  paddasslem5  34590  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  4atex2-0cOLDN  34846  ltrn11at  34913  trlval3  34954  cdlemd3  34967  cdleme7aa  35009  cdleme7b  35011  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme16aN  35026  cdleme11dN  35029  cdleme11e  35030  cdleme11l  35036  cdleme11  35037  cdleme12  35038  cdleme14  35040  cdleme15a  35041  cdleme15c  35043  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme17c  35055  cdleme18c  35060  cdlemeda  35065  cdlemednpq  35066  cdleme19a  35071  cdleme19c  35073  cdleme20aN  35077  cdleme20bN  35078  cdleme20l1  35088  cdleme20l2  35089  cdleme22aa  35107  cdleme22a  35108  cdleme22g  35116  cdleme23b  35118  cdleme23c  35119  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme28b  35139  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35h  35224  cdleme35sn2aw  35226  cdleme38m  35231  cdleme40n  35236  cdleme41sn3aw  35242  cdleme41sn4aw  35243  cdlemeg46gfre  35300  cdlemf1  35329  cdlemg1cex  35356  cdlemg2ce  35360  cdlemg4d  35381  cdlemg4  35385  cdlemg7fvN  35392  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg11aq  35406  cdlemg10a  35408  cdlemg12a  35411  cdlemg12b  35412  cdlemg12d  35414  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg14f  35421  cdlemg14g  35422  cdlemg17b  35430  cdlemg17dN  35431  cdlemg17e  35433  cdlemg17pq  35440  cdlemg17iqN  35442  cdlemg18c  35448  cdlemg18d  35449  cdlemg19a  35451  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg28a  35461  cdlemg31b0N  35462  cdlemg27b  35464  cdlemg31c  35467  cdlemg33b0  35469  cdlemg28  35472  cdlemg33a  35474  cdlemg33  35479  cdlemg35  35481  cdlemg36  35482  cdlemg44a  35499  cdlemg46  35503  cdlemh2  35584  cdlemh  35585  cdlemj1  35589  cdlemk5  35604  cdlemk6  35605  cdlemki  35609  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemkole  35621  cdlemk14  35622  cdlemk16  35625  cdlemk1u  35627  cdlemk18  35636  cdlemk19  35637  cdlemk7u  35638  cdlemk11u  35639  cdlemk33N  35677  cdlemkid2  35692  cdlemkfid3N  35693  cdlemk11ta  35697  cdlemk11tc  35713  cdlemk45  35715  cdlemk46  35716  cdlemk47  35717  cdlemk52  35722  cdlemk53a  35723  cdlemk54  35726  cdlemk55a  35727  cdleml1N  35744  cdleml3N  35746  cdlemn7  35972  cdlemn8  35973  cdlemn10  35975  dihordlem7  35983  dihordlem7b  35984  dihord1  35987  dihord10  35992  dihord11c  35993  dihord2  35996  hlhilphllem  36731  fmuldfeq  39219
  Copyright terms: Public domain W3C validator