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

Theorem anim12ci 615
Description: Variant of anim12i 614 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
anim12i.1 (𝜑𝜓)
anim12i.2 (𝜒𝜃)
Assertion
Ref Expression
anim12ci ((𝜑𝜒) → (𝜃𝜓))

Proof of Theorem anim12ci
StepHypRef Expression
1 anim12i.2 . . 3 (𝜒𝜃)
2 anim12i.1 . . 3 (𝜑𝜓)
31, 2anim12i 614 . 2 ((𝜒𝜑) → (𝜃𝜓))
43ancoms 461 1 ((𝜑𝜒) → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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
This theorem is referenced by:  anim1ci  617  2exeuv  2713  2exeu  2727  2rexreu  3752  ideqg  5721  dfco2a  6098  frnssb  6884  fliftval  7068  omlimcl  8203  funsnfsupp  8856  ltrnq  10400  ltsrpr  10498  difelfznle  13020  nelfzo  13042  muladdmodid  13278  modmulmodr  13304  modsumfzodifsn  13311  ccatsymb  13935  swrdnd0  14018  pfxsuffeqwrdeq  14059  pfxccatin12lem2a  14088  repswswrd  14145  cshwidxm  14169  s3iunsndisj  14327  lcmftp  15979  ncoprmlnprm  16067  modprm0  16141  dvdsprmpweqle  16221  difsqpwdvds  16222  brssc  17083  resmhm  17984  mhmco  17987  idresefmnd  18063  gasubg  18431  idrespermg  18538  rhmco  19488  resrhm  19563  cply1mul  20461  dmatmul  21105  scmatf1  21139  slesolinv  21288  slesolinvbi  21289  slesolex  21290  cramerimplem3  21293  cramerimp  21294  chfacfscmulgsum  21467  chfacfpmmulgsum  21471  bwth  22017  nmhmco  23364  chpchtsum  25794  gausslemma2dlem1a  25940  2lgslem1a1  25964  2sq2  26008  dchrisum0lem1  26091  subusgr  27070  isuvtx  27176  iscplgredg  27198  structtocusgr  27227  crctcshwlkn0  27598  crctcsh  27601  rusgrnumwwlk  27753  clwlkclwwlklem3  27778  clwwlkf1  27827  eucrctshift  28021  frgr3v  28053  frgrwopreglem5a  28089  numclwwlk3  28163  frgrreg  28172  ex-ceil  28226  occon2  29064  bnj1110  32254  satfv1lem  32609  relowlssretop  34643  poimirlem16  34907  poimirlem19  34910  poimirlem30  34921  pr2cv  39907  itgspltprt  42264  or2expropbilem1  43268  iccpartiltu  43583  iccpartgt  43588  ich2exprop  43634  goldbachthlem1  43708  goldbachthlem2  43709  nn0e  43863  nneven  43864  stgoldbwt  43942  bgoldbtbndlem3  43973  bgoldbtbndlem4  43974  bgoldbtbnd  43975  isomushgr  43992  isomuspgrlem1  43993  resmgmhm  44066  mgmhmco  44069  rnghmco  44179  ztprmneprm  44396  nn0sumltlt  44399  ldepspr  44529  m1modmmod  44582  blennngt2o2  44653  line2xlem  44741  aacllem  44903
  Copyright terms: Public domain W3C validator