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

Theorem anim12ci 588
Description: Variant of anim12i 587 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 587 . 2 ((𝜒𝜑) → (𝜃𝜓))
43ancoms 467 1 ((𝜑𝜒) → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  2exeu  2532  ideqg  5179  dfco2a  5534  frnssb  6279  fliftval  6440  omlimcl  7518  funsnfsupp  8155  ltrnq  9653  ltsrpr  9750  difelfznle  12273  nelfzo  12295  muladdmodid  12523  modmulmodr  12549  modsumfzodifsn  12556  hash2prd  13060  swrdccatin12lem2a  13278  repswswrd  13324  cshwidxm  13347  s3iunsndisj  13497  lcmftp  15129  ncoprmlnprm  15216  modprm0  15290  difsqpwdvds  15371  brssc  16239  resmhm  17124  mhmco  17127  gasubg  17500  idrespermg  17596  rhmco  18502  resrhm  18574  cply1mul  19427  dmatmul  20060  scmatf1  20094  slesolinv  20243  slesolinvbi  20244  slesolex  20245  cramerimplem3  20248  cramerimp  20249  chfacfscmulgsum  20422  chfacfpmmulgsum  20426  bwth  20961  nmhmco  22298  chpchtsum  24657  gausslemma2dlem1a  24803  2lgslem1a1  24827  dchrisum0lem1  24918  wlkdvspthlem  25899  clwlkisclwwlklem0  26078  clwwlkf1  26086  wwlksubclwwlk  26094  clwlkfclwwlk  26133  clwlkf1clwwlklem  26138  vdgrf  26187  frgra3v  26291  frgrancvvdeqlem3  26321  frghash2spot  26352  numclwwlk3  26398  numclwwlk5  26401  frgrareg  26406  ex-ceil  26459  occon2  27333  bnj1110  30106  relowlssretop  32186  poimirlem16  32394  poimirlem19  32397  poimirlem30  32408  itgspltprt  38671  2rexreu  39634  iccpartiltu  39761  iccpartgt  39766  goldbachthlem1  39796  goldbachthlem2  39797  nn0e  39947  stgoldbwt  39999  bgoldbtbndlem3  40024  bgoldbtbndlem4  40025  bgoldbtbnd  40026  subusgr  40511  isuvtxa  40619  iscplgredg  40637  crctcsh1wlkn0  41022  crctcsh  41025  rusgrnumwwlk  41176  clwlkclwwlklem3  41208  clwwlksf1  41222  clwlksfclwwlk  41267  clwlksf1clwwlklem  41273  eucrctshift  41409  frgr3v  41443  frgrncvvdeqlem3  41469  av-numclwwlk3  41537  av-frgrareg  41546  resmgmhm  41586  mgmhmco  41589  rnghmco  41695  ztprmneprm  41916  nn0sumltlt  41919  ldepspr  42054  m1modmmod  42108  blennngt2o2  42182  aacllem  42315
  Copyright terms: Public domain W3C validator