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  2547  ideqg  5262  dfco2a  5623  frnssb  6377  fliftval  6551  omlimcl  7643  funsnfsupp  8284  ltrnq  9786  ltsrpr  9883  difelfznle  12437  nelfzo  12459  muladdmodid  12693  modmulmodr  12719  modsumfzodifsn  12726  hash2prd  13240  swrdccatin12lem2a  13466  repswswrd  13512  cshwidxm  13535  s3iunsndisj  13688  lcmftp  15330  ncoprmlnprm  15417  modprm0  15491  difsqpwdvds  15572  brssc  16455  resmhm  17340  mhmco  17343  gasubg  17716  idrespermg  17812  rhmco  18718  resrhm  18790  cply1mul  19645  dmatmul  20284  scmatf1  20318  slesolinv  20467  slesolinvbi  20468  slesolex  20469  cramerimplem3  20472  cramerimp  20473  chfacfscmulgsum  20646  chfacfpmmulgsum  20650  bwth  21194  nmhmco  22541  chpchtsum  24925  gausslemma2dlem1a  25071  2lgslem1a1  25095  dchrisum0lem1  25186  subusgr  26162  isuvtxa  26276  iscplgredg  26294  structtocusgr  26323  crctcshwlkn0  26694  crctcsh  26697  rusgrnumwwlk  26851  clwlkclwwlklem3  26883  clwwlksf1  26897  clwlksfclwwlk  26942  clwlksf1clwwlklem  26948  eucrctshift  27083  frgr3v  27119  numclwwlk3  27213  frgrreg  27222  ex-ceil  27275  occon2  28117  bnj1110  31024  relowlssretop  33182  poimirlem16  33396  poimirlem19  33399  poimirlem30  33410  itgspltprt  39958  2rexreu  40948  iccpartiltu  41122  iccpartgt  41127  goldbachthlem1  41222  goldbachthlem2  41223  nn0e  41373  stgoldbwt  41429  bgoldbtbndlem3  41460  bgoldbtbndlem4  41461  bgoldbtbnd  41462  resmgmhm  41563  mgmhmco  41566  rnghmco  41672  ztprmneprm  41890  nn0sumltlt  41893  ldepspr  42027  m1modmmod  42081  blennngt2o2  42151  aacllem  42312
  Copyright terms: Public domain W3C validator