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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 1083 . 2 ((𝜓𝜒𝜃) → 𝜃)
213ad2ant2 1103 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 1056
This theorem is referenced by:  simpl23  1161  simpr23  1170  simp123  1215  simp223  1224  simp323  1233  funtpgOLD  5981  omeulem1  7707  elfiun  8377  cofsmo  9129  modexp  13039  iscatd2  16389  funcoppc  16582  funcres  16603  catcisolem  16803  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  pmtrprfv3  17920  mdetunilem3  20468  mdetunilem4  20469  mdetuni0  20475  mdetmul  20477  prdsxmetlem  22220  isosctrlem3  24595  isosctr  24596  f1otrg  25796  colinearalg  25835  ax5seglem6  25859  ax5seg  25863  axpasch  25866  axeuclid  25888  uhgr2edg  26145  clwwlkccat  27332  ogrpsub  29845  ogrpsublt  29850  rhmdvd  29949  bnj966  31140  bnj967  31141  mclspps  31607  cgrtr  32224  cgrtr3  32226  ofscom  32239  btwnxfr  32288  colinearxfr  32307  lineext  32308  brofs2  32309  brifs2  32310  fscgr  32312  linecgr  32313  btwnconn1lem1  32319  btwnconn1lem2  32320  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem5  32323  btwnconn1lem6  32324  btwnconn1lem7  32325  seglecgr12im  32342  seglecgr12  32343  segletr  32346  broutsideof3  32358  outsideofeq  32362  lineunray  32379  eqlkr  34704  omlmod1i2N  34865  cvrcmp2  34889  cvlexch2  34934  cvlexchb2  34936  cvlatexchb2  34940  cvlatexch1  34941  cvlatexch2  34942  cvlatexch3  34943  cvlsupr7  34953  cvlsupr8  34954  atnlej1  34983  atnlej2  34984  2llnneN  35013  cvratlem  35025  atcvrneN  35034  atcvrj1  35035  atlelt  35042  2atjm  35049  3noncolr2  35053  3noncolr1N  35054  hlatcon2  35056  3dimlem2  35063  3dim1  35071  3dim2  35072  1cvrat  35080  ps-1  35081  ps-2  35082  2atjlej  35083  hlatexch3N  35084  ps-2b  35086  3atlem1  35087  3atlem2  35088  3atlem6  35092  llnle  35122  2atm  35131  ps-2c  35132  lplni2  35141  lplnle  35144  lplnnle2at  35145  lplnri3N  35159  llncvrlpln2  35161  2atmat  35165  2llnjaN  35170  2llnm2N  35172  2llnm4  35174  2llnmeqat  35175  lvolnle3at  35186  4atlem0ae  35198  4atlem0be  35199  4atlem3b  35202  4atlem9  35207  4atlem10a  35208  4atlem10  35210  4atlem11a  35211  4atlem12a  35214  4at  35217  4at2  35218  lplncvrlvol2  35219  2lplnm2N  35225  2llnma1b  35390  2llnma1  35391  2llnma3r  35392  2llnma2  35393  2llnma2rN  35394  cdlema1N  35395  cdlema2N  35396  paddasslem2  35425  paddasslem15  35438  paddasslem16  35439  pmodlem1  35450  pmod2iN  35453  hlmod1i  35460  atmod2i1  35465  atmod2i2  35466  atmod3i1  35468  atmod3i2  35469  atmod4i1  35470  atmod4i2  35471  llnexchb2  35473  dalawlem3  35477  dalawlem4  35478  dalawlem5  35479  dalawlem6  35480  dalawlem7  35481  dalawlem8  35482  dalawlem9  35483  dalawlem11  35485  dalawlem13  35487  dalawlem15  35489  osumcllem7N  35566  osumcllem9N  35568  osumcllem11N  35570  pl42lem1N  35583  4atex  35680  4atex2-0aOLDN  35682  4atex2-0bOLDN  35683  4atex2-0cOLDN  35684  trlval4  35793  cdlemc5  35800  cdlemd5  35807  cdlemd6  35808  cdleme00a  35814  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme4  35843  cdleme4a  35844  cdleme16aN  35864  cdleme11c  35866  cdleme11g  35870  cdleme11h  35871  cdleme12  35876  cdleme0nex  35895  cdleme18a  35896  cdleme18b  35897  cdleme18c  35898  cdleme18d  35900  cdleme20zN  35906  cdleme20y  35907  cdleme19a  35908  cdleme19b  35909  cdleme19d  35911  cdleme19e  35912  cdleme20aN  35914  cdleme20c  35916  cdleme20d  35917  cdleme20i  35922  cdleme20j  35923  cdleme20l1  35925  cdleme20l2  35926  cdleme20m  35928  cdleme21b  35931  cdleme21c  35932  cdleme21j  35941  cdleme22aa  35944  cdleme22a  35945  cdleme22eALTN  35950  cdleme26e  35964  cdleme26fALTN  35967  cdleme26f  35968  cdleme26f2ALTN  35969  cdleme26f2  35970  cdleme27N  35974  cdleme28a  35975  cdleme28b  35976  cdleme30a  35983  cdlemefs45eN  36036  cdleme32c  36048  cdleme32e  36050  cdleme35h  36061  cdleme36a  36065  cdleme36m  36066  cdleme37m  36067  cdleme41sn3aw  36079  cdleme41sn4aw  36080  cdleme41fva11  36082  cdleme42k  36089  cdleme43cN  36096  cdleme43dN  36097  cdleme46f2g1  36099  cdlemeg47rv2  36115  cdlemeg46sfg  36125  cdlemeg46fjgN  36126  cdlemeg46rjgN  36127  cdlemeg46fjv  36128  cdlemeg46frv  36130  cdlemeg46vrg  36132  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemeg46gfv  36135  cdleme50trn2a  36155  cdlemg2fv2  36205  cdlemg4a  36213  cdlemg4e  36219  cdlemg4f  36220  cdlemg8b  36233  cdlemg8c  36234  cdlemg9a  36237  cdlemg9b  36238  cdlemg9  36239  cdlemg10a  36245  cdlemg12a  36248  cdlemg12b  36249  cdlemg12c  36250  cdlemg12  36255  cdlemg17dN  36268  cdlemg17dALTN  36269  cdlemg17e  36270  cdlemg17i  36274  cdlemg17ir  36275  cdlemg17pq  36277  cdlemg17bq  36278  cdlemg17iqN  36279  cdlemg17  36282  cdlemg18b  36284  cdlemg18c  36285  cdlemg18d  36286  cdlemg18  36287  cdlemg19  36289  cdlemg21  36291  cdlemg28a  36298  cdlemg31b0a  36300  cdlemg33b0  36306  cdlemg35  36318  cdlemg44a  36336  cdlemh  36422  cdlemi2  36424  cdlemj1  36426  cdlemk5a  36440  cdlemk5  36441  cdlemki  36446  cdlemkvcl  36447  cdlemk10  36448  cdlemksv2  36452  cdlemk7  36453  cdlemk11  36454  cdlemk12  36455  cdlemk15  36460  cdlemk16a  36461  cdlemk16  36462  cdlemk5u  36466  cdlemk6u  36467  cdlemk18  36473  cdlemk19  36474  cdlemk7u  36475  cdlemk11u  36476  cdlemk12u  36477  cdlemk21N  36478  cdlemk20  36479  cdlemkoatnle-2N  36480  cdlemk13-2N  36481  cdlemkole-2N  36482  cdlemk14-2N  36483  cdlemk15-2N  36484  cdlemk16-2N  36485  cdlemk17-2N  36486  cdlemk18-2N  36491  cdlemk19-2N  36492  cdlemk22  36498  cdlemk30  36499  cdlemk28-3  36513  cdlemk33N  36514  cdlemkfid1N  36526  cdlemkid1  36527  cdlemky  36531  cdlemk11ta  36534  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk47  36554  cdlemk48  36555  cdlemk49  36556  cdlemk50  36557  cdlemk51  36558  cdlemk52  36559  cdlemk53a  36560  cdlemk53b  36561  cdlemk53  36562  cdlemk54  36563  cdlemk55a  36564  cdlemkyyN  36567  cdlemk43N  36568  cdlemk55u1  36570  cdlemk55u  36571  cdlemk39u1  36572  cdlemk19u1  36574  cdleml1N  36581  cdleml2N  36582  cdleml3N  36583  dia2dimlem6  36675  cdlemn2  36801  cdlemn2a  36802  cdlemn5pre  36806  cdlemn11pre  36816  dihjustlem  36822  dihjust  36823  dihmeetlem15N  36927  lclkrlem2y  37137  relexpxpnnidm  38312
  Copyright terms: Public domain W3C validator