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

Theorem anim12ci 608
Description: Variant of anim12i 607 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 607 . 2 ((𝜒𝜑) → (𝜃𝜓))
43ancoms 451 1 ((𝜑𝜒) → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  anim1ci  610  2exeu  2706  ideqg  5478  dfco2a  5855  frnssb  6618  fliftval  6795  omlimcl  7899  funsnfsupp  8542  ltrnq  10090  ltsrpr  10187  difelfznle  12707  nelfzo  12729  muladdmodid  12964  modmulmodr  12990  modsumfzodifsn  12997  swrdnd0  13685  swrdccatin12lem2a  13786  repswswrd  13863  cshwidxm  13892  s3iunsndisj  14049  lcmftp  15683  ncoprmlnprm  15768  modprm0  15842  difsqpwdvds  15923  brssc  16787  resmhm  17673  mhmco  17676  gasubg  18046  idrespermg  18142  rhmco  19054  resrhm  19126  cply1mul  19985  dmatmul  20628  scmatf1  20662  slesolinv  20812  slesolinvbi  20813  slesolex  20814  cramerimplem3  20818  cramerimp  20819  chfacfscmulgsum  20992  chfacfpmmulgsum  20996  bwth  21541  nmhmco  22887  chpchtsum  25295  gausslemma2dlem1a  25441  2lgslem1a1  25465  dchrisum0lem1  25556  subusgr  26522  isuvtx  26640  isuvtxaOLD  26641  iscplgredg  26666  structtocusgr  26695  crctcshwlkn0  27071  crctcsh  27074  rusgrnumwwlk  27266  clwlkclwwlklem3  27293  clwwlkf1OLD  27357  clwwlkf1  27362  clwlksfclwwlkOLD  27402  clwlksf1clwwlklemOLD  27408  eucrctshift  27587  frgr3v  27623  frgrwopreglem5a  27659  numclwwlk3  27769  frgrreg  27778  ex-ceil  27832  occon2  28671  bnj1110  31566  relowlssretop  33708  poimirlem16  33913  poimirlem19  33916  poimirlem30  33927  itgspltprt  40933  2rexreu  41957  iccpartiltu  42193  iccpartgt  42198  goldbachthlem1  42234  goldbachthlem2  42235  nn0e  42385  stgoldbwt  42441  bgoldbtbndlem3  42472  bgoldbtbndlem4  42473  bgoldbtbnd  42474  isomushgr  42491  isomuspgrlem1  42492  resmgmhm  42592  mgmhmco  42595  rnghmco  42701  ztprmneprm  42919  nn0sumltlt  42922  ldepspr  43056  m1modmmod  43110  blennngt2o2  43180  aacllem  43344
  Copyright terms: Public domain W3C validator