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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 1137 . 2 ((𝜒𝜃𝜏) → 𝜃)
213ad2ant3 1135 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  simp132  1309  simp232  1318  simp332  1327  eqfunresadj  7301  smogt  8305  axdc3lem4  10347  bitsfzo  16275  frlmphl  21140  mdetunilem4  21916  mdetuni0  21922  mdetmul  21924  decpmatmullem  22072  logfacbnd3  26523  logexprlim  26525  log2sumbnd  26844  nosupfv  27006  nosupres  27007  noinffv  27021  noinfres  27022  ax5seg  27716  numclwwlk1lem2foa  29127  iocinioc2  31508  totprob  32839  cgrtr  34515  cgrtr3  34517  ofscom  34530  cgrextend  34531  segconeq  34533  ifscgr  34567  colinearxfr  34598  brofs2  34600  brifs2  34601  fscgr  34603  btwnconn1lem2  34611  btwnconn1lem9  34618  btwnconn1lem10  34619  btwnconn1lem11  34620  btwnconn1lem12  34621  brsegle2  34632  seglecgr12im  34633  seglecgr12  34634  segletr  34637  outsideofeq  34653  ivthALT  34745  lshpkrlem5  37514  lshpkrlem6  37515  atbtwnexOLDN  37848  atbtwnex  37849  4noncolr3  37854  3dimlem3a  37861  3dim1  37868  3dim2  37869  1cvrat  37877  2atjlej  37880  hlatexch4  37882  ps-2b  37883  2atm  37928  ps-2c  37929  2atmat  37962  4atlem10  38007  4atlem11b  38009  4atlem11  38010  4at  38014  4at2  38015  2lplnja  38020  2lplnj  38021  dalemswapyz  38057  dalem-ddly  38087  cdlemb  38195  paddasslem5  38225  pmodlem1  38247  dalawlem1  38272  dalawlem3  38274  dalawlem4  38275  dalawlem5  38276  dalawlem6  38277  dalawlem7  38278  dalawlem8  38279  dalawlem9  38280  dalawlem11  38282  dalawlem12  38283  dalawlem15  38286  osumcllem5N  38361  osumcllem6N  38362  lhpexle3lem  38412  lhpmcvr4N  38427  lhpmcvr6N  38429  4atexlemex6  38475  4atex2  38478  4atex2-0bOLDN  38480  4atex2-0cOLDN  38481  ltrn11at  38548  trlval3  38588  cdlemd3  38601  cdleme7aa  38643  cdleme7b  38645  cdleme7c  38646  cdleme7d  38647  cdleme7e  38648  cdleme7ga  38649  cdleme7  38650  cdleme16aN  38660  cdleme11dN  38663  cdleme11e  38664  cdleme11l  38670  cdleme11  38671  cdleme12  38672  cdleme14  38674  cdleme15a  38675  cdleme15c  38677  cdleme16c  38681  cdleme16d  38682  cdleme16e  38683  cdleme16f  38684  cdleme17c  38689  cdleme18c  38694  cdlemeda  38699  cdlemednpq  38700  cdleme19a  38704  cdleme19c  38706  cdleme20aN  38710  cdleme20bN  38711  cdleme20l1  38721  cdleme20l2  38722  cdleme22aa  38740  cdleme22a  38741  cdleme22g  38749  cdleme23b  38751  cdleme23c  38752  cdleme26fALTN  38763  cdleme26f  38764  cdleme26f2ALTN  38765  cdleme26f2  38766  cdleme28b  38772  cdleme32b  38843  cdleme32c  38844  cdleme32e  38846  cdleme35h  38857  cdleme35sn2aw  38859  cdleme38m  38864  cdleme40n  38869  cdleme41sn3aw  38875  cdleme41sn4aw  38876  cdlemeg46gfre  38933  cdlemf1  38962  cdlemg1cex  38989  cdlemg2ce  38993  cdlemg4d  39014  cdlemg4  39018  cdlemg7fvN  39025  cdlemg8b  39029  cdlemg8c  39030  cdlemg9a  39033  cdlemg11aq  39039  cdlemg10a  39041  cdlemg12a  39044  cdlemg12b  39045  cdlemg12d  39047  cdlemg12g  39050  cdlemg12  39051  cdlemg13a  39052  cdlemg13  39053  cdlemg14f  39054  cdlemg14g  39055  cdlemg17b  39063  cdlemg17dN  39064  cdlemg17e  39066  cdlemg17pq  39073  cdlemg17iqN  39075  cdlemg18c  39081  cdlemg18d  39082  cdlemg19a  39084  cdlemg19  39085  cdlemg21  39087  cdlemg27a  39093  cdlemg28a  39094  cdlemg31b0N  39095  cdlemg27b  39097  cdlemg31c  39100  cdlemg33b0  39102  cdlemg28  39105  cdlemg33a  39107  cdlemg33  39112  cdlemg35  39114  cdlemg36  39115  cdlemg44a  39132  cdlemg46  39136  cdlemh2  39217  cdlemh  39218  cdlemj1  39222  cdlemk5  39237  cdlemk6  39238  cdlemki  39242  cdlemksv2  39248  cdlemk7  39249  cdlemk11  39250  cdlemkole  39254  cdlemk14  39255  cdlemk16  39258  cdlemk1u  39260  cdlemk18  39269  cdlemk19  39270  cdlemk7u  39271  cdlemk11u  39272  cdlemk33N  39310  cdlemkid2  39325  cdlemkfid3N  39326  cdlemk11ta  39330  cdlemk11tc  39346  cdlemk45  39348  cdlemk46  39349  cdlemk47  39350  cdlemk52  39355  cdlemk53a  39356  cdlemk54  39359  cdlemk55a  39360  cdleml1N  39377  cdleml3N  39379  cdlemn7  39604  cdlemn8  39605  cdlemn10  39607  dihordlem7  39615  dihordlem7b  39616  dihord1  39619  dihord10  39624  dihord11c  39625  dihord2  39628  hlhilphllem  40364  fmuldfeq  43725  seposep  46859  iscnrm3rlem8  46881  iscnrm3llem2  46884
  Copyright terms: Public domain W3C validator