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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 1132 . 2 ((𝜓𝜒𝜃) → 𝜃)
213ad2ant2 1128 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 1083
This theorem is referenced by:  simp123  1301  simp223  1310  simp323  1319  omeulem1  8200  elfiun  8886  cofsmo  9683  modexp  13591  iscatd2  16944  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  pmtrprfv3  18574  mdetunilem3  21215  mdetunilem4  21216  mdetuni0  21222  mdetmul  21224  prdsxmetlem  22970  isosctrlem3  25390  isosctr  25391  f1otrg  26649  colinearalg  26688  ax5seglem6  26712  ax5seg  26716  axpasch  26719  axeuclid  26741  uhgr2edg  26982  clwwlkccat  27760  ogrpsub  30710  ogrpsublt  30715  rhmdvd  30887  bnj966  32204  bnj967  32205  mclspps  32819  cgrtr  33441  cgrtr3  33443  ofscom  33456  btwnxfr  33505  colinearxfr  33524  lineext  33525  brofs2  33526  brifs2  33527  fscgr  33529  linecgr  33530  btwnconn1lem1  33536  btwnconn1lem2  33537  btwnconn1lem3  33538  btwnconn1lem4  33539  btwnconn1lem5  33540  btwnconn1lem6  33541  btwnconn1lem7  33542  seglecgr12im  33559  seglecgr12  33560  segletr  33563  broutsideof3  33575  outsideofeq  33579  lineunray  33596  eqlkr  36222  omlmod1i2N  36383  cvrcmp2  36407  cvlexch2  36452  cvlexchb2  36454  cvlatexchb2  36458  cvlatexch1  36459  cvlatexch2  36460  cvlatexch3  36461  cvlsupr7  36471  cvlsupr8  36472  atnlej1  36502  atnlej2  36503  2llnneN  36532  cvratlem  36544  atcvrneN  36553  atcvrj1  36554  atlelt  36561  2atjm  36568  3noncolr2  36572  3noncolr1N  36573  hlatcon2  36575  3dimlem2  36582  3dim1  36590  3dim2  36591  1cvrat  36599  ps-1  36600  ps-2  36601  2atjlej  36602  hlatexch3N  36603  ps-2b  36605  3atlem1  36606  3atlem2  36607  3atlem6  36611  llnle  36641  2atm  36650  ps-2c  36651  lplni2  36660  lplnle  36663  lplnnle2at  36664  lplnri3N  36678  llncvrlpln2  36680  2atmat  36684  2llnjaN  36689  2llnm2N  36691  2llnm4  36693  2llnmeqat  36694  lvolnle3at  36705  4atlem0ae  36717  4atlem0be  36718  4atlem3b  36721  4atlem9  36726  4atlem10a  36727  4atlem10  36729  4atlem11a  36730  4atlem12a  36733  4at  36736  4at2  36737  lplncvrlvol2  36738  2lplnm2N  36744  2llnma1b  36909  2llnma1  36910  2llnma3r  36911  2llnma2  36912  2llnma2rN  36913  cdlema1N  36914  cdlema2N  36915  paddasslem2  36944  paddasslem15  36957  paddasslem16  36958  pmodlem1  36969  pmod2iN  36972  hlmod1i  36979  atmod2i1  36984  atmod2i2  36985  atmod3i1  36987  atmod3i2  36988  atmod4i1  36989  atmod4i2  36990  llnexchb2  36992  dalawlem3  36996  dalawlem4  36997  dalawlem5  36998  dalawlem6  36999  dalawlem7  37000  dalawlem8  37001  dalawlem9  37002  dalawlem11  37004  dalawlem13  37006  dalawlem15  37008  osumcllem7N  37085  osumcllem9N  37087  osumcllem11N  37089  pl42lem1N  37102  4atex  37199  4atex2-0aOLDN  37201  4atex2-0bOLDN  37202  4atex2-0cOLDN  37203  trlval4  37311  cdlemc5  37318  cdlemd5  37325  cdlemd6  37326  cdleme00a  37332  cdleme3g  37357  cdleme3h  37358  cdleme3  37360  cdleme4  37361  cdleme4a  37362  cdleme16aN  37382  cdleme11c  37384  cdleme11g  37388  cdleme11h  37389  cdleme12  37394  cdleme0nex  37413  cdleme18a  37414  cdleme18b  37415  cdleme18c  37416  cdleme18d  37418  cdleme20zN  37424  cdleme20y  37425  cdleme19a  37426  cdleme19b  37427  cdleme19d  37429  cdleme19e  37430  cdleme20aN  37432  cdleme20c  37434  cdleme20d  37435  cdleme20i  37440  cdleme20j  37441  cdleme20l1  37443  cdleme20l2  37444  cdleme20m  37446  cdleme21b  37449  cdleme21c  37450  cdleme21j  37459  cdleme22aa  37462  cdleme22a  37463  cdleme22eALTN  37468  cdleme26e  37482  cdleme26fALTN  37485  cdleme26f  37486  cdleme26f2ALTN  37487  cdleme26f2  37488  cdleme27N  37492  cdleme28a  37493  cdleme28b  37494  cdleme30a  37501  cdlemefs45eN  37554  cdleme32c  37566  cdleme32e  37568  cdleme35h  37579  cdleme36a  37583  cdleme36m  37584  cdleme37m  37585  cdleme41sn3aw  37597  cdleme41sn4aw  37598  cdleme41fva11  37600  cdleme42k  37607  cdleme43cN  37614  cdleme43dN  37615  cdleme46f2g1  37617  cdlemeg47rv2  37633  cdlemeg46sfg  37643  cdlemeg46fjgN  37644  cdlemeg46rjgN  37645  cdlemeg46fjv  37646  cdlemeg46frv  37648  cdlemeg46vrg  37650  cdlemeg46rgv  37651  cdlemeg46req  37652  cdlemeg46gfv  37653  cdleme50trn2a  37673  cdlemg2fv2  37723  cdlemg4a  37731  cdlemg4e  37737  cdlemg4f  37738  cdlemg8b  37751  cdlemg8c  37752  cdlemg9a  37755  cdlemg9b  37756  cdlemg9  37757  cdlemg10a  37763  cdlemg12a  37766  cdlemg12b  37767  cdlemg12c  37768  cdlemg12  37773  cdlemg17dN  37786  cdlemg17dALTN  37787  cdlemg17e  37788  cdlemg17i  37792  cdlemg17ir  37793  cdlemg17pq  37795  cdlemg17bq  37796  cdlemg17iqN  37797  cdlemg17  37800  cdlemg18b  37802  cdlemg18c  37803  cdlemg18d  37804  cdlemg18  37805  cdlemg19  37807  cdlemg21  37809  cdlemg28a  37816  cdlemg31b0a  37818  cdlemg33b0  37824  cdlemg35  37836  cdlemg44a  37854  cdlemh  37940  cdlemi2  37942  cdlemj1  37944  cdlemk5a  37958  cdlemk5  37959  cdlemki  37964  cdlemkvcl  37965  cdlemk10  37966  cdlemksv2  37970  cdlemk7  37971  cdlemk11  37972  cdlemk12  37973  cdlemk15  37978  cdlemk16a  37979  cdlemk16  37980  cdlemk5u  37984  cdlemk6u  37985  cdlemk18  37991  cdlemk19  37992  cdlemk7u  37993  cdlemk11u  37994  cdlemk12u  37995  cdlemk21N  37996  cdlemk20  37997  cdlemkoatnle-2N  37998  cdlemk13-2N  37999  cdlemkole-2N  38000  cdlemk14-2N  38001  cdlemk15-2N  38002  cdlemk16-2N  38003  cdlemk17-2N  38004  cdlemk18-2N  38009  cdlemk19-2N  38010  cdlemk22  38016  cdlemk30  38017  cdlemk28-3  38031  cdlemk33N  38032  cdlemkfid1N  38044  cdlemkid1  38045  cdlemky  38049  cdlemk11ta  38052  cdlemk35s-id  38061  cdlemk39s-id  38063  cdlemk47  38072  cdlemk48  38073  cdlemk49  38074  cdlemk50  38075  cdlemk51  38076  cdlemk52  38077  cdlemk53a  38078  cdlemk53b  38079  cdlemk53  38080  cdlemk54  38081  cdlemk55a  38082  cdlemkyyN  38085  cdlemk43N  38086  cdlemk55u1  38088  cdlemk55u  38089  cdlemk39u1  38090  cdlemk19u1  38092  cdleml1N  38099  cdleml2N  38100  cdleml3N  38101  dia2dimlem6  38192  cdlemn2  38318  cdlemn2a  38319  cdlemn5pre  38323  cdlemn11pre  38333  dihjustlem  38339  dihjust  38340  dihmeetlem15N  38444  lclkrlem2y  38654  relexpxpnnidm  40033
  Copyright terms: Public domain W3C validator