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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 1133 . 2 ((𝜒𝜃𝜏) → 𝜃)
213ad2ant3 1131 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  simp132  1305  simp232  1314  simp332  1323  smogt  8007  axdc3lem4  9878  bitsfzo  15787  frlmphl  20928  mdetunilem4  21227  mdetuni0  21233  mdetmul  21235  decpmatmullem  21382  logfacbnd3  25802  logexprlim  25804  log2sumbnd  26123  ax5seg  26727  numclwwlk1lem2foa  28136  iocinioc2  30505  totprob  31689  eqfunresadj  33008  nosupfv  33210  nosupres  33211  cgrtr  33457  cgrtr3  33459  ofscom  33472  cgrextend  33473  segconeq  33475  ifscgr  33509  colinearxfr  33540  brofs2  33542  brifs2  33543  fscgr  33545  btwnconn1lem2  33553  btwnconn1lem9  33560  btwnconn1lem10  33561  btwnconn1lem11  33562  btwnconn1lem12  33563  brsegle2  33574  seglecgr12im  33575  seglecgr12  33576  segletr  33579  outsideofeq  33595  ivthALT  33687  lshpkrlem5  36254  lshpkrlem6  36255  atbtwnexOLDN  36587  atbtwnex  36588  4noncolr3  36593  3dimlem3a  36600  3dim1  36607  3dim2  36608  1cvrat  36616  2atjlej  36619  hlatexch4  36621  ps-2b  36622  2atm  36667  ps-2c  36668  2atmat  36701  4atlem10  36746  4atlem11b  36748  4atlem11  36749  4at  36753  4at2  36754  2lplnja  36759  2lplnj  36760  dalemswapyz  36796  dalem-ddly  36826  cdlemb  36934  paddasslem5  36964  pmodlem1  36986  dalawlem1  37011  dalawlem3  37013  dalawlem4  37014  dalawlem5  37015  dalawlem6  37016  dalawlem7  37017  dalawlem8  37018  dalawlem9  37019  dalawlem11  37021  dalawlem12  37022  dalawlem15  37025  osumcllem5N  37100  osumcllem6N  37101  lhpexle3lem  37151  lhpmcvr4N  37166  lhpmcvr6N  37168  4atexlemex6  37214  4atex2  37217  4atex2-0bOLDN  37219  4atex2-0cOLDN  37220  ltrn11at  37287  trlval3  37327  cdlemd3  37340  cdleme7aa  37382  cdleme7b  37384  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme16aN  37399  cdleme11dN  37402  cdleme11e  37403  cdleme11l  37409  cdleme11  37410  cdleme12  37411  cdleme14  37413  cdleme15a  37414  cdleme15c  37416  cdleme16c  37420  cdleme16d  37421  cdleme16e  37422  cdleme16f  37423  cdleme17c  37428  cdleme18c  37433  cdlemeda  37438  cdlemednpq  37439  cdleme19a  37443  cdleme19c  37445  cdleme20aN  37449  cdleme20bN  37450  cdleme20l1  37460  cdleme20l2  37461  cdleme22aa  37479  cdleme22a  37480  cdleme22g  37488  cdleme23b  37490  cdleme23c  37491  cdleme26fALTN  37502  cdleme26f  37503  cdleme26f2ALTN  37504  cdleme26f2  37505  cdleme28b  37511  cdleme32b  37582  cdleme32c  37583  cdleme32e  37585  cdleme35h  37596  cdleme35sn2aw  37598  cdleme38m  37603  cdleme40n  37608  cdleme41sn3aw  37614  cdleme41sn4aw  37615  cdlemeg46gfre  37672  cdlemf1  37701  cdlemg1cex  37728  cdlemg2ce  37732  cdlemg4d  37753  cdlemg4  37757  cdlemg7fvN  37764  cdlemg8b  37768  cdlemg8c  37769  cdlemg9a  37772  cdlemg11aq  37778  cdlemg10a  37780  cdlemg12a  37783  cdlemg12b  37784  cdlemg12d  37786  cdlemg12g  37789  cdlemg12  37790  cdlemg13a  37791  cdlemg13  37792  cdlemg14f  37793  cdlemg14g  37794  cdlemg17b  37802  cdlemg17dN  37803  cdlemg17e  37805  cdlemg17pq  37812  cdlemg17iqN  37814  cdlemg18c  37820  cdlemg18d  37821  cdlemg19a  37823  cdlemg19  37824  cdlemg21  37826  cdlemg27a  37832  cdlemg28a  37833  cdlemg31b0N  37834  cdlemg27b  37836  cdlemg31c  37839  cdlemg33b0  37841  cdlemg28  37844  cdlemg33a  37846  cdlemg33  37851  cdlemg35  37853  cdlemg36  37854  cdlemg44a  37871  cdlemg46  37875  cdlemh2  37956  cdlemh  37957  cdlemj1  37961  cdlemk5  37976  cdlemk6  37977  cdlemki  37981  cdlemksv2  37987  cdlemk7  37988  cdlemk11  37989  cdlemkole  37993  cdlemk14  37994  cdlemk16  37997  cdlemk1u  37999  cdlemk18  38008  cdlemk19  38009  cdlemk7u  38010  cdlemk11u  38011  cdlemk33N  38049  cdlemkid2  38064  cdlemkfid3N  38065  cdlemk11ta  38069  cdlemk11tc  38085  cdlemk45  38087  cdlemk46  38088  cdlemk47  38089  cdlemk52  38094  cdlemk53a  38095  cdlemk54  38098  cdlemk55a  38099  cdleml1N  38116  cdleml3N  38118  cdlemn7  38343  cdlemn8  38344  cdlemn10  38346  dihordlem7  38354  dihordlem7b  38355  dihord1  38358  dihord10  38363  dihord11c  38364  dihord2  38367  hlhilphllem  39099  fmuldfeq  41870
  Copyright terms: Public domain W3C validator