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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 1132 . 2 ((𝜒𝜃𝜏) → 𝜃)
213ad2ant3 1130 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  simpl32OLD  1330  simpr32OLD  1348  simp132  1394  simp232  1403  simp332  1412  smogt  7635  axdc3lem4  9488  bitsfzo  15380  frlmphl  20343  mdetunilem4  20644  mdetuni0  20650  mdetmul  20652  decpmatmullem  20799  logfacbnd3  25169  logexprlim  25171  log2sumbnd  25454  ax5seg  26039  numclwlk1lem2foa  27535  iocinioc2  29872  totprob  30820  eqfunresadj  31988  nosupfv  32180  nosupres  32181  cgrtr  32427  cgrtr3  32429  ofscom  32442  cgrextend  32443  segconeq  32445  ifscgr  32479  colinearxfr  32510  brofs2  32512  brifs2  32513  fscgr  32515  btwnconn1lem2  32523  btwnconn1lem9  32530  btwnconn1lem10  32531  btwnconn1lem11  32532  btwnconn1lem12  32533  brsegle2  32544  seglecgr12im  32545  seglecgr12  32546  segletr  32549  outsideofeq  32565  ivthALT  32658  lshpkrlem5  34923  lshpkrlem6  34924  atbtwnexOLDN  35255  atbtwnex  35256  4noncolr3  35261  3dimlem3a  35268  3dim1  35275  3dim2  35276  1cvrat  35284  2atjlej  35287  hlatexch4  35289  ps-2b  35290  2atm  35335  ps-2c  35336  2atmat  35369  4atlem10  35414  4atlem11b  35416  4atlem11  35417  4at  35421  4at2  35422  2lplnja  35427  2lplnj  35428  dalemswapyz  35464  dalem-ddly  35494  cdlemb  35602  paddasslem5  35632  pmodlem1  35654  dalawlem1  35679  dalawlem3  35681  dalawlem4  35682  dalawlem5  35683  dalawlem6  35684  dalawlem7  35685  dalawlem8  35686  dalawlem9  35687  dalawlem11  35689  dalawlem12  35690  dalawlem15  35693  osumcllem5N  35768  osumcllem6N  35769  lhpexle3lem  35819  lhpmcvr4N  35834  lhpmcvr6N  35836  4atexlemex6  35882  4atex2  35885  4atex2-0bOLDN  35887  4atex2-0cOLDN  35888  ltrn11at  35955  trlval3  35996  cdlemd3  36009  cdleme7aa  36051  cdleme7b  36053  cdleme7c  36054  cdleme7d  36055  cdleme7e  36056  cdleme7ga  36057  cdleme7  36058  cdleme16aN  36068  cdleme11dN  36071  cdleme11e  36072  cdleme11l  36078  cdleme11  36079  cdleme12  36080  cdleme14  36082  cdleme15a  36083  cdleme15c  36085  cdleme16c  36089  cdleme16d  36090  cdleme16e  36091  cdleme16f  36092  cdleme17c  36097  cdleme18c  36102  cdlemeda  36107  cdlemednpq  36108  cdleme19a  36112  cdleme19c  36114  cdleme20aN  36118  cdleme20bN  36119  cdleme20l1  36129  cdleme20l2  36130  cdleme22aa  36148  cdleme22a  36149  cdleme22g  36157  cdleme23b  36159  cdleme23c  36160  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme28b  36180  cdleme32b  36251  cdleme32c  36252  cdleme32e  36254  cdleme35h  36265  cdleme35sn2aw  36267  cdleme38m  36272  cdleme40n  36277  cdleme41sn3aw  36283  cdleme41sn4aw  36284  cdlemeg46gfre  36341  cdlemf1  36370  cdlemg1cex  36397  cdlemg2ce  36401  cdlemg4d  36422  cdlemg4  36426  cdlemg7fvN  36433  cdlemg8b  36437  cdlemg8c  36438  cdlemg9a  36441  cdlemg11aq  36447  cdlemg10a  36449  cdlemg12a  36452  cdlemg12b  36453  cdlemg12d  36455  cdlemg12g  36458  cdlemg12  36459  cdlemg13a  36460  cdlemg13  36461  cdlemg14f  36462  cdlemg14g  36463  cdlemg17b  36471  cdlemg17dN  36472  cdlemg17e  36474  cdlemg17pq  36481  cdlemg17iqN  36483  cdlemg18c  36489  cdlemg18d  36490  cdlemg19a  36492  cdlemg19  36493  cdlemg21  36495  cdlemg27a  36501  cdlemg28a  36502  cdlemg31b0N  36503  cdlemg27b  36505  cdlemg31c  36508  cdlemg33b0  36510  cdlemg28  36513  cdlemg33a  36515  cdlemg33  36520  cdlemg35  36522  cdlemg36  36523  cdlemg44a  36540  cdlemg46  36544  cdlemh2  36625  cdlemh  36626  cdlemj1  36630  cdlemk5  36645  cdlemk6  36646  cdlemki  36650  cdlemksv2  36656  cdlemk7  36657  cdlemk11  36658  cdlemkole  36662  cdlemk14  36663  cdlemk16  36666  cdlemk1u  36668  cdlemk18  36677  cdlemk19  36678  cdlemk7u  36679  cdlemk11u  36680  cdlemk33N  36718  cdlemkid2  36733  cdlemkfid3N  36734  cdlemk11ta  36738  cdlemk11tc  36754  cdlemk45  36756  cdlemk46  36757  cdlemk47  36758  cdlemk52  36763  cdlemk53a  36764  cdlemk54  36767  cdlemk55a  36768  cdleml1N  36785  cdleml3N  36787  cdlemn7  37013  cdlemn8  37014  cdlemn10  37016  dihordlem7  37024  dihordlem7b  37025  dihord1  37028  dihord10  37033  dihord11c  37034  dihord2  37037  hlhilphllem  37772  fmuldfeq  40337
  Copyright terms: Public domain W3C validator