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

Theorem anim12ci 575
Description: Variant of anim12i 574 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
anim12i.1  |-  ( ph  ->  ps )
anim12i.2  |-  ( ch 
->  th )
Assertion
Ref Expression
anim12ci  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )

Proof of Theorem anim12ci
StepHypRef Expression
1 anim12i.2 . . 3  |-  ( ch 
->  th )
2 anim12i.1 . . 3  |-  ( ph  ->  ps )
31, 2anim12i 574 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 459 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  2exeu  2389  dfco2a  5354  frnssb  6075  fliftval  6234  omlimcl  7305  funsnfsupp  7933  supmaxlemOLD  8008  ltrnq  9430  ltsrpr  9527  difelfznle  11935  nelfzo  11956  muladdmodid  12169  hash2prd  12667  swrdccatin12lem2a  12878  repswswrd  12924  cshwidxm  12946  lcmftp  14658  ncoprmlnprm  14726  modprm0  14805  brssc  15768  resmhm  16655  mhmco  16658  gasubg  17005  idrespermg  17101  rhmco  18014  resrhm  18086  cply1mul  18936  dmatmul  19571  scmatf1  19605  slesolinv  19754  slesolinvbi  19755  slesolex  19756  cramerimplem3  19759  cramerimp  19760  chfacfscmulgsum  19933  chfacfpmmulgsum  19937  bwth  20474  nmhmco  21826  chpchtsum  24196  dchrisum0lem1  24403  wlkdvspthlem  25386  clwlkisclwwlklem0  25565  clwwlkf1  25573  wwlksubclwwlk  25581  clwlkfclwwlk  25621  clwlkf1clwwlklem  25626  vdgrf  25675  frgra3v  25779  frgrancvvdeqlem3  25809  frghash2spot  25840  numclwwlk3  25886  numclwwlk5  25889  frgrareg  25894  occon2  26990  bnj1110  29840  relowlssretop  31811  poimirlem16  32001  poimirlem19  32004  poimirlem30  32015  itgspltprt  37894  2rexreu  38644  iccpartiltu  38774  iccpartgt  38779  nn0e  38864  stgoldbwt  38915  bgoldbtbndlem3  38940  bgoldbtbndlem4  38941  bgoldbtbnd  38942  subusgr  39411  isuvtxa  39517  iscplgredg  39535  resmgmhm  40071  mgmhmco  40074  rnghmco  40180  ztprmneprm  40401  nn0sumltlt  40404  ldepspr  40539  m1modmmod  40597  blennngt2o2  40676  aacllem  40813
  Copyright terms: Public domain W3C validator