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

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

Proof of Theorem simp31
StepHypRef Expression
1 simp1 1059 . 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:  simpl31  1140  simpr31  1149  simp131  1194  simp231  1203  simp331  1212  smogt  7409  frlmphl  20039  mdetuni0  20346  mdetmul  20348  gsummatr01lem3  20382  decpmatmullem  20495  tsmsxp  21868  log2sumbnd  25133  ax5seg  25718  wlkoniswlk  26426  iocinioc2  29385  totprob  30270  nosires  31577  cgrtr  31741  cgrtr3  31743  ofscom  31756  cgrextend  31757  segconeq  31759  ifscgr  31793  btwnxfr  31805  colinearxfr  31824  brofs2  31826  brifs2  31827  fscgr  31829  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem7  31842  btwnconn1lem8  31843  btwnconn1lem9  31844  btwnconn1lem10  31845  btwnconn1lem11  31846  btwnconn1lem12  31847  seglecgr12im  31859  seglecgr12  31860  segletr  31863  outsideofeq  31879  ivthALT  31972  lshpkrlem5  33881  lshpkrlem6  33882  exatleN  34170  atbtwn  34212  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  2atmat  34327  4atlem11b  34374  4atlem11  34375  4at  34379  4at2  34380  2lplnja  34385  2lplnj  34386  dalemswapyz  34422  dalemccnedd  34453  cdlemb  34560  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  4atex2  34843  4atex2-0bOLDN  34845  4atex3  34847  ltrn11at  34913  trlval3  34954  cdlemd3  34967  cdleme0moN  34992  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  cdleme15b  35042  cdleme15c  35043  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme17c  35055  cdleme18c  35060  cdleme18d  35062  cdlemeda  35065  cdleme19a  35071  cdleme19b  35072  cdleme19c  35073  cdleme20aN  35077  cdleme20bN  35078  cdleme20d  35080  cdleme20i  35085  cdleme20j  35086  cdleme20l1  35088  cdleme20l2  35089  cdleme21d  35098  cdleme21e  35099  cdleme21f  35100  cdleme22aa  35107  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f2  35115  cdleme22g  35116  cdleme23b  35118  cdleme26eALTN  35129  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme28a  35138  cdleme28b  35139  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35h  35224  cdleme35sn2aw  35226  cdleme41sn3aw  35242  cdleme41sn4aw  35243  cdlemeg46gfre  35300  cdlemf1  35329  cdlemg1cex  35356  cdlemg2ce  35360  cdlemg4d  35381  cdlemg4e  35382  cdlemg4f  35383  cdlemg4  35385  cdlemg6d  35389  cdlemg6e  35390  cdlemg7fvN  35392  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg9b  35401  cdlemg9  35402  cdlemg11aq  35406  cdlemg10a  35408  cdlemg12a  35411  cdlemg12b  35412  cdlemg12c  35413  cdlemg12d  35414  cdlemg13  35420  cdlemg14f  35421  cdlemg14g  35422  cdlemg17b  35430  cdlemg17dN  35431  cdlemg17e  35433  cdlemg17i  35437  cdlemg17pq  35440  cdlemg17iqN  35442  cdlemg18c  35448  cdlemg18d  35449  cdlemg18  35450  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg31b0N  35462  cdlemg27b  35464  cdlemg31c  35467  cdlemg33b0  35469  cdlemg33c0  35470  cdlemg33  35479  cdlemg35  35481  cdlemg43  35498  cdlemg44a  35499  cdlemg46  35503  cdlemh2  35584  cdlemh  35585  cdlemj1  35589  cdlemk3  35601  cdlemk5  35604  cdlemk6  35605  cdlemki  35609  cdlemksv2  35615  cdlemk12  35618  cdlemk15  35623  cdlemk16  35625  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  cdlemk20-2N  35660  cdlemk22  35661  cdlemk30  35662  cdlemk31  35664  cdlemk24-3  35671  cdlemkid2  35692  cdlemkfid3N  35693  cdlemk11ta  35697  cdlemkid3N  35701  cdlemk11tc  35713  cdlemk45  35715  cdlemk46  35716  cdlemk47  35717  cdlemk52  35722  cdlemk53a  35723  cdlemk53b  35724  cdleml1N  35744  cdleml3N  35746  cdlemn7  35972  cdlemn10  35975  dihordlem7  35983  dihord1  35987  dihord11c  35993  dihord2  35996  hlhilphllem  36731  fmuldfeq  39219
  Copyright terms: Public domain W3C validator