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

Theorem anim12ci 590
Description: Variant of anim12i 589 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 589 . 2 ((𝜒𝜑) → (𝜃𝜓))
43ancoms 469 1 ((𝜑𝜒) → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  2exeu  2548  ideqg  5243  dfco2a  5604  frnssb  6357  fliftval  6531  omlimcl  7618  funsnfsupp  8259  ltrnq  9761  ltsrpr  9858  difelfznle  12410  nelfzo  12432  muladdmodid  12666  modmulmodr  12692  modsumfzodifsn  12699  hash2prd  13211  swrdccatin12lem2a  13438  repswswrd  13484  cshwidxm  13507  s3iunsndisj  13657  lcmftp  15292  ncoprmlnprm  15379  modprm0  15453  difsqpwdvds  15534  brssc  16414  resmhm  17299  mhmco  17302  gasubg  17675  idrespermg  17771  rhmco  18677  resrhm  18749  cply1mul  19604  dmatmul  20243  scmatf1  20277  slesolinv  20426  slesolinvbi  20427  slesolex  20428  cramerimplem3  20431  cramerimp  20432  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  bwth  21153  nmhmco  22500  chpchtsum  24878  gausslemma2dlem1a  25024  2lgslem1a1  25048  dchrisum0lem1  25139  subusgr  26108  isuvtxa  26216  iscplgredg  26234  structtocusgr  26263  crctcshwlkn0  26616  crctcsh  26619  rusgrnumwwlk  26771  clwlkclwwlklem3  26803  clwwlksf1  26817  clwlksfclwwlk  26862  clwlksf1clwwlklem  26868  eucrctshift  27003  frgr3v  27037  frgrncvvdeqlem3  27063  numclwwlk3  27131  frgrreg  27140  ex-ceil  27193  occon2  28035  bnj1110  30811  relowlssretop  32882  poimirlem16  33096  poimirlem19  33099  poimirlem30  33110  itgspltprt  39532  2rexreu  40519  iccpartiltu  40686  iccpartgt  40691  goldbachthlem1  40786  goldbachthlem2  40787  nn0e  40937  stgoldbwt  40989  bgoldbtbndlem3  41014  bgoldbtbndlem4  41015  bgoldbtbnd  41016  resmgmhm  41116  mgmhmco  41119  rnghmco  41225  ztprmneprm  41443  nn0sumltlt  41446  ldepspr  41580  m1modmmod  41634  blennngt2o2  41708  aacllem  41880
  Copyright terms: Public domain W3C validator