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

Theorem anim12ci 593
 Description: Variant of anim12i 592 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 592 . 2 ((𝜒𝜑) → (𝜃𝜓))
43ancoms 455 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 197  df-an 383 This theorem is referenced by:  2exeu  2697  ideqg  5412  dfco2a  5779  frnssb  6533  fliftval  6708  omlimcl  7811  funsnfsupp  8454  ltrnq  10002  ltsrpr  10099  difelfznle  12660  nelfzo  12682  muladdmodid  12917  modmulmodr  12943  modsumfzodifsn  12950  swrdccatin12lem2a  13693  repswswrd  13739  cshwidxm  13762  s3iunsndisj  13916  lcmftp  15556  ncoprmlnprm  15642  modprm0  15716  difsqpwdvds  15797  brssc  16680  resmhm  17566  mhmco  17569  gasubg  17941  idrespermg  18037  rhmco  18946  resrhm  19018  cply1mul  19878  dmatmul  20520  scmatf1  20554  slesolinv  20704  slesolinvbi  20705  slesolex  20706  cramerimplem3  20710  cramerimp  20711  chfacfscmulgsum  20884  chfacfpmmulgsum  20888  bwth  21433  nmhmco  22779  chpchtsum  25164  gausslemma2dlem1a  25310  2lgslem1a1  25334  dchrisum0lem1  25425  subusgr  26403  isuvtx  26521  isuvtxaOLD  26522  iscplgredg  26547  structtocusgr  26576  crctcshwlkn0  26948  crctcsh  26951  rusgrnumwwlk  27121  clwlkclwwlklem3  27148  clwwlkf1  27202  clwlksfclwwlkOLD  27240  clwlksf1clwwlklemOLD  27246  eucrctshift  27420  frgr3v  27454  frgrwopreglem5a  27490  numclwwlk3  27578  frgrreg  27587  ex-ceil  27641  occon2  28481  bnj1110  31382  relowlssretop  33541  poimirlem16  33751  poimirlem19  33754  poimirlem30  33765  itgspltprt  40706  2rexreu  41699  iccpartiltu  41876  iccpartgt  41881  goldbachthlem1  41975  goldbachthlem2  41976  nn0e  42126  stgoldbwt  42182  bgoldbtbndlem3  42213  bgoldbtbndlem4  42214  bgoldbtbnd  42215  resmgmhm  42316  mgmhmco  42319  rnghmco  42425  ztprmneprm  42643  nn0sumltlt  42646  ldepspr  42780  m1modmmod  42834  blennngt2o2  42904  aacllem  43068
 Copyright terms: Public domain W3C validator