Theorem anim12ci 591

Description: Variant of anim12i 590 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

Step	Hyp	Ref	Expression
1		anim12i.2	. . 3 |- ( ch -> th )
2		anim12i.1	. . 3 |- ( ph -> ps )
3	1, 2	anim12i 590	. 2 |- ( ( ch /\ ph ) -> ( th /\ ps ) )
4	3	ancoms 469	1 |- ( ( ph /\ ch ) -> ( th /\ ps ) )

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  2549  ideqg  5273  dfco2a  5635  frnssb  6391  fliftval  6566  omlimcl  7658  funsnfsupp  8299  ltrnq  9801  ltsrpr  9898  difelfznle  12453  nelfzo  12475  muladdmodid  12710  modmulmodr  12736  modsumfzodifsn  12743  hash2prd  13257  swrdccatin12lem2a  13485  repswswrd  13531  cshwidxm  13554  s3iunsndisj  13707  lcmftp  15349  ncoprmlnprm  15436  modprm0  15510  difsqpwdvds  15591  brssc  16474  resmhm  17359  mhmco  17362  gasubg  17735  idrespermg  17831  rhmco  18737  resrhm  18809  cply1mul  19664  dmatmul  20303  scmatf1  20337  slesolinv  20486  slesolinvbi  20487  slesolex  20488  cramerimplem3  20491  cramerimp  20492  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  bwth  21213  nmhmco  22560  chpchtsum  24944  gausslemma2dlem1a  25090  2lgslem1a1  25114  dchrisum0lem1  25205  subusgr  26181  isuvtxa  26295  iscplgredg  26313  structtocusgr  26342  crctcshwlkn0  26713  crctcsh  26716  rusgrnumwwlk  26870  clwlkclwwlklem3  26902  clwwlksf1  26917  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  eucrctshift  27103  frgr3v  27139  frgrwopreglem5a  27175  numclwwlk3OLD  27242  numclwwlk3  27243  frgrreg  27252  ex-ceil  27305  occon2  28147  bnj1110  31050  relowlssretop  33211  poimirlem16  33425  poimirlem19  33428  poimirlem30  33439  itgspltprt  40195  2rexreu  41185  iccpartiltu  41358  iccpartgt  41363  goldbachthlem1  41457  goldbachthlem2  41458  nn0e  41608  stgoldbwt  41664  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  resmgmhm  41798  mgmhmco  41801  rnghmco  41907  ztprmneprm  42125  nn0sumltlt  42128  ldepspr  42262  m1modmmod  42316  blennngt2o2  42386  aacllem  42547