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

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

Proof of Theorem simp21
StepHypRef Expression
1 simp1 1128 . 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:  simp121  1297  simp221  1306  simp321  1315  omeulem1  8198  cofsmo  9680  axdc4lem  9866  0catg  16948  funcoppc  17135  funcres  17156  catcisolem  17356  1stfcl  17437  2ndfcl  17438  prfcl  17443  evlfcl  17462  curf1cl  17468  curfcl  17472  hofcl  17499  mulgdirlem  18198  mdetunilem4  21154  mdetuni0  21160  mdetmul  21162  prdsxmetlem  22907  isosctrlem3  25325  isosctr  25326  amgmlem  25495  f1otrg  26585  colinearalg  26624  ax5seglem6  26648  ax5seg  26652  axpasch  26655  axeuclidlem  26676  axeuclid  26677  uhgr2edg  26918  numclwlk1lem2  28077  ogrpsub  30645  ogrpaddlt  30646  ogrpsublt  30650  rhmdvd  30822  bnj1128  32160  mclspps  32729  nosupbnd2lem1  33113  cgrtr  33351  cgrtr3  33353  ofscom  33366  segconeq  33369  ifscgr  33403  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  lineelsb2  33507  linecom  33509  lshpkrlem5  36132  omlmod1i2N  36278  cvrnbtwn3  36294  cvrcmp  36301  cvrcmp2  36302  cvlexch2  36347  cvlexchb2  36349  cvlatexchb2  36353  cvlatexch2  36355  cvlatexch3  36356  cvlsupr7  36366  atnlej1  36397  atnlej2  36398  2llnneN  36427  cvratlem  36439  atcvrneN  36448  atcvrj1  36449  atlelt  36456  2atjm  36463  3noncolr2  36467  3noncolr1N  36468  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  3atlem5  36505  3atlem6  36506  llnle  36536  2atm  36545  ps-2c  36546  lplni2  36555  lplnle  36558  lplnnle2at  36559  lplnri3N  36573  llncvrlpln2  36575  2atmat  36579  2llnm2N  36586  2llnm4  36588  2llnmeqat  36589  lvolnle3at  36600  4atlem0ae  36612  4atlem0be  36613  4atlem3b  36616  4atlem9  36621  4atlem10a  36622  4atlem10  36624  4atlem11a  36625  4atlem12a  36628  4at2  36632  2lplnm2N  36639  lneq2at  36796  2llnma1b  36804  2llnma1  36805  2llnma3r  36806  2llnma2  36807  2llnma2rN  36808  cdlema1N  36809  paddasslem2  36839  paddasslem15  36852  paddasslem16  36853  pmodlem1  36864  pmodlem2  36865  pmod2iN  36867  hlmod1i  36874  atmod1i1m  36876  atmod2i1  36879  atmod2i2  36880  atmod3i1  36882  atmod3i2  36883  atmod4i1  36884  atmod4i2  36885  llnexchb2lem  36886  llnexch2N  36888  dalawlem3  36891  dalawlem4  36892  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem8  36896  dalawlem9  36897  dalawlem11  36899  dalawlem12  36900  dalawlem13  36901  dalawlem15  36903  osumcllem9N  36982  pl42lem1N  36997  4atexlems  37070  4atex2  37095  4atex2-0bOLDN  37097  trlval4  37206  cdlemc5  37213  cdlemc6  37214  cdlemd2  37217  cdlemd4  37219  cdlemd6  37221  cdleme00a  37227  cdleme0e  37235  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4  37256  cdleme4a  37257  cdleme5  37258  cdleme9  37271  cdleme16aN  37277  cdleme11c  37279  cdleme11e  37281  cdleme11g  37283  cdleme11h  37284  cdleme11j  37285  cdleme11k  37286  cdleme11l  37287  cdleme11  37288  cdleme12  37289  cdleme14  37291  cdleme15c  37294  cdleme16b  37297  cdleme16c  37298  cdleme16d  37299  cdleme16e  37300  cdleme16f  37301  cdleme0nex  37308  cdleme18a  37309  cdleme18c  37311  cdleme18d  37313  cdlemednpq  37317  cdlemednuN  37318  cdleme20zN  37319  cdleme20y  37320  cdleme19a  37321  cdleme19b  37322  cdleme19d  37324  cdleme19e  37325  cdleme20aN  37327  cdleme20bN  37328  cdleme20c  37329  cdleme20d  37330  cdleme20f  37332  cdleme20g  37333  cdleme20i  37335  cdleme20j  37336  cdleme20l1  37338  cdleme20l2  37339  cdleme20l  37340  cdleme20m  37341  cdleme21b  37344  cdleme21c  37345  cdleme21e  37349  cdleme21f  37350  cdleme22a  37358  cdleme22b  37359  cdleme22e  37362  cdleme22eALTN  37363  cdleme22f  37364  cdleme26eALTN  37379  cdleme26fALTN  37380  cdleme26f  37381  cdleme26f2ALTN  37382  cdleme26f2  37383  cdleme27N  37387  cdleme28a  37388  cdleme28b  37389  cdleme30a  37396  cdleme43fsv1snlem  37438  cdlemefs31fv1  37442  cdlemefs45eN  37449  cdleme32b  37460  cdleme32c  37461  cdleme32d  37462  cdleme35h  37474  cdleme36a  37478  cdleme36m  37479  cdleme37m  37480  cdleme40m  37485  cdleme40n  37486  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  cdlemg4a  37626  cdlemg4d  37631  cdlemg4e  37632  cdlemg4f  37633  cdlemg4g  37634  cdlemg4  37635  cdlemg6d  37639  cdlemg6e  37640  cdlemg8b  37646  cdlemg8c  37647  cdlemg9a  37650  cdlemg9b  37651  cdlemg10a  37658  cdlemg10  37659  cdlemg12a  37661  cdlemg12b  37662  cdlemg12f  37666  cdlemg12g  37667  cdlemg12  37668  cdlemg17dN  37681  cdlemg17dALTN  37682  cdlemg17e  37683  cdlemg17f  37684  cdlemg17g  37685  cdlemg17h  37686  cdlemg17i  37687  cdlemg17pq  37690  cdlemg17iqN  37692  cdlemg17  37695  cdlemg18b  37697  cdlemg18c  37698  cdlemg19a  37701  cdlemg19  37702  cdlemg28a  37711  cdlemg27b  37714  cdlemg28b  37721  cdlemg28  37722  cdlemg33a  37724  cdlemg33b  37725  cdlemg33c  37726  cdlemg33d  37727  cdlemg33e  37728  cdlemg33  37729  cdlemg35  37731  cdlemg36  37732  cdlemg44a  37749  cdlemh  37835  cdlemi2  37837  cdlemj1  37839  tendocan  37842  cdlemk5a  37853  cdlemki  37859  cdlemkvcl  37860  cdlemk10  37861  cdlemksv2  37865  cdlemkole  37871  cdlemk14  37872  cdlemk15  37873  cdlemk16a  37874  cdlemk16  37875  cdlemk17  37876  cdlemk18  37886  cdlemk19  37887  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  cdlemk30  37912  cdlemk18-3N  37918  cdlemk23-3  37920  cdlemk25-3  37922  cdlemk27-3  37925  cdlemk37  37932  cdlemkfid1N  37939  cdlemkid1  37940  cdlemky  37944  cdlemk11ta  37947  cdlemk47  37967  cdlemk48  37968  cdlemk49  37969  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  cdlemk53a  37973  cdlemk54  37976  cdlemk39u1  37985  cdlemk19u1  37987  cdleml1N  37994  cdleml2N  37995  cdleml3N  37996  dia2dimlem6  38087  cdlemn2  38213  cdlemn2a  38214  cdlemn5pre  38218  cdlemn10  38224  cdlemn11c  38227  cdlemn11pre  38228  dihjustlem  38234  dihjust  38235  lclkrlem2y  38549  relexpmulnn  39934  lincreslvec3  44435  amgmwlem  44801
  Copyright terms: Public domain W3C validator