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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 1130 . 2 ((𝜓𝜒𝜃) → 𝜃)
213ad2ant2 1126 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp123  1299  simp223  1308  simp323  1317  omeulem1  8198  elfiun  8883  cofsmo  9680  modexp  13589  iscatd2  16942  funcoppc  17135  funcres  17156  catcisolem  17356  1stfcl  17437  2ndfcl  17438  prfcl  17443  evlfcl  17462  curf1cl  17468  curfcl  17472  hofcl  17499  pmtrprfv3  18513  mdetunilem3  21153  mdetunilem4  21154  mdetuni0  21160  mdetmul  21162  prdsxmetlem  22907  isosctrlem3  25325  isosctr  25326  f1otrg  26585  colinearalg  26624  ax5seglem6  26648  ax5seg  26652  axpasch  26655  axeuclid  26677  uhgr2edg  26918  clwwlkccat  27696  ogrpsub  30645  ogrpsublt  30650  rhmdvd  30822  bnj966  32116  bnj967  32117  mclspps  32729  cgrtr  33351  cgrtr3  33353  ofscom  33366  btwnxfr  33415  colinearxfr  33434  lineext  33435  brofs2  33436  brifs2  33437  fscgr  33439  linecgr  33440  btwnconn1lem1  33446  btwnconn1lem2  33447  btwnconn1lem3  33448  btwnconn1lem4  33449  btwnconn1lem5  33450  btwnconn1lem6  33451  btwnconn1lem7  33452  seglecgr12im  33469  seglecgr12  33470  segletr  33473  broutsideof3  33485  outsideofeq  33489  lineunray  33506  eqlkr  36117  omlmod1i2N  36278  cvrcmp2  36302  cvlexch2  36347  cvlexchb2  36349  cvlatexchb2  36353  cvlatexch1  36354  cvlatexch2  36355  cvlatexch3  36356  cvlsupr7  36366  cvlsupr8  36367  atnlej1  36397  atnlej2  36398  2llnneN  36427  cvratlem  36439  atcvrneN  36448  atcvrj1  36449  atlelt  36456  2atjm  36463  3noncolr2  36467  3noncolr1N  36468  hlatcon2  36470  3dimlem2  36477  3dim1  36485  3dim2  36486  1cvrat  36494  ps-1  36495  ps-2  36496  2atjlej  36497  hlatexch3N  36498  ps-2b  36500  3atlem1  36501  3atlem2  36502  3atlem6  36506  llnle  36536  2atm  36545  ps-2c  36546  lplni2  36555  lplnle  36558  lplnnle2at  36559  lplnri3N  36573  llncvrlpln2  36575  2atmat  36579  2llnjaN  36584  2llnm2N  36586  2llnm4  36588  2llnmeqat  36589  lvolnle3at  36600  4atlem0ae  36612  4atlem0be  36613  4atlem3b  36616  4atlem9  36621  4atlem10a  36622  4atlem10  36624  4atlem11a  36625  4atlem12a  36628  4at  36631  4at2  36632  lplncvrlvol2  36633  2lplnm2N  36639  2llnma1b  36804  2llnma1  36805  2llnma3r  36806  2llnma2  36807  2llnma2rN  36808  cdlema1N  36809  cdlema2N  36810  paddasslem2  36839  paddasslem15  36852  paddasslem16  36853  pmodlem1  36864  pmod2iN  36867  hlmod1i  36874  atmod2i1  36879  atmod2i2  36880  atmod3i1  36882  atmod3i2  36883  atmod4i1  36884  atmod4i2  36885  llnexchb2  36887  dalawlem3  36891  dalawlem4  36892  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem8  36896  dalawlem9  36897  dalawlem11  36899  dalawlem13  36901  dalawlem15  36903  osumcllem7N  36980  osumcllem9N  36982  osumcllem11N  36984  pl42lem1N  36997  4atex  37094  4atex2-0aOLDN  37096  4atex2-0bOLDN  37097  4atex2-0cOLDN  37098  trlval4  37206  cdlemc5  37213  cdlemd5  37220  cdlemd6  37221  cdleme00a  37227  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4  37256  cdleme4a  37257  cdleme16aN  37277  cdleme11c  37279  cdleme11g  37283  cdleme11h  37284  cdleme12  37289  cdleme0nex  37308  cdleme18a  37309  cdleme18b  37310  cdleme18c  37311  cdleme18d  37313  cdleme20zN  37319  cdleme20y  37320  cdleme19a  37321  cdleme19b  37322  cdleme19d  37324  cdleme19e  37325  cdleme20aN  37327  cdleme20c  37329  cdleme20d  37330  cdleme20i  37335  cdleme20j  37336  cdleme20l1  37338  cdleme20l2  37339  cdleme20m  37341  cdleme21b  37344  cdleme21c  37345  cdleme21j  37354  cdleme22aa  37357  cdleme22a  37358  cdleme22eALTN  37363  cdleme26e  37377  cdleme26fALTN  37380  cdleme26f  37381  cdleme26f2ALTN  37382  cdleme26f2  37383  cdleme27N  37387  cdleme28a  37388  cdleme28b  37389  cdleme30a  37396  cdlemefs45eN  37449  cdleme32c  37461  cdleme32e  37463  cdleme35h  37474  cdleme36a  37478  cdleme36m  37479  cdleme37m  37480  cdleme41sn3aw  37492  cdleme41sn4aw  37493  cdleme41fva11  37495  cdleme42k  37502  cdleme43cN  37509  cdleme43dN  37510  cdleme46f2g1  37512  cdlemeg47rv2  37528  cdlemeg46sfg  37538  cdlemeg46fjgN  37539  cdlemeg46rjgN  37540  cdlemeg46fjv  37541  cdlemeg46frv  37543  cdlemeg46vrg  37545  cdlemeg46rgv  37546  cdlemeg46req  37547  cdlemeg46gfv  37548  cdleme50trn2a  37568  cdlemg2fv2  37618  cdlemg4a  37626  cdlemg4e  37632  cdlemg4f  37633  cdlemg8b  37646  cdlemg8c  37647  cdlemg9a  37650  cdlemg9b  37651  cdlemg9  37652  cdlemg10a  37658  cdlemg12a  37661  cdlemg12b  37662  cdlemg12c  37663  cdlemg12  37668  cdlemg17dN  37681  cdlemg17dALTN  37682  cdlemg17e  37683  cdlemg17i  37687  cdlemg17ir  37688  cdlemg17pq  37690  cdlemg17bq  37691  cdlemg17iqN  37692  cdlemg17  37695  cdlemg18b  37697  cdlemg18c  37698  cdlemg18d  37699  cdlemg18  37700  cdlemg19  37702  cdlemg21  37704  cdlemg28a  37711  cdlemg31b0a  37713  cdlemg33b0  37719  cdlemg35  37731  cdlemg44a  37749  cdlemh  37835  cdlemi2  37837  cdlemj1  37839  cdlemk5a  37853  cdlemk5  37854  cdlemki  37859  cdlemkvcl  37860  cdlemk10  37861  cdlemksv2  37865  cdlemk7  37866  cdlemk11  37867  cdlemk12  37868  cdlemk15  37873  cdlemk16a  37874  cdlemk16  37875  cdlemk5u  37879  cdlemk6u  37880  cdlemk18  37886  cdlemk19  37887  cdlemk7u  37888  cdlemk11u  37889  cdlemk12u  37890  cdlemk21N  37891  cdlemk20  37892  cdlemkoatnle-2N  37893  cdlemk13-2N  37894  cdlemkole-2N  37895  cdlemk14-2N  37896  cdlemk15-2N  37897  cdlemk16-2N  37898  cdlemk17-2N  37899  cdlemk18-2N  37904  cdlemk19-2N  37905  cdlemk22  37911  cdlemk30  37912  cdlemk28-3  37926  cdlemk33N  37927  cdlemkfid1N  37939  cdlemkid1  37940  cdlemky  37944  cdlemk11ta  37947  cdlemk35s-id  37956  cdlemk39s-id  37958  cdlemk47  37967  cdlemk48  37968  cdlemk49  37969  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  cdlemk53a  37973  cdlemk53b  37974  cdlemk53  37975  cdlemk54  37976  cdlemk55a  37977  cdlemkyyN  37980  cdlemk43N  37981  cdlemk55u1  37983  cdlemk55u  37984  cdlemk39u1  37985  cdlemk19u1  37987  cdleml1N  37994  cdleml2N  37995  cdleml3N  37996  dia2dimlem6  38087  cdlemn2  38213  cdlemn2a  38214  cdlemn5pre  38218  cdlemn11pre  38228  dihjustlem  38234  dihjust  38235  dihmeetlem15N  38339  lclkrlem2y  38549  relexpxpnnidm  39928
  Copyright terms: Public domain W3C validator