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

Theorem anim12ci 565
Description: Variant of anim12i 564 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 564 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 451 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  2exeu  2368  dfco2a  5490  fliftval  6189  omlimcl  7219  funsnfsupp  7845  supmaxlemOLD  7916  ltrnq  9346  ltsrpr  9443  difelfznle  11793  nelfzo  11809  muladdmodid  12019  swrdccatin12lem2a  12704  repswswrd  12750  cshwidxm  12772  modprm0  14417  brssc  15305  resmhm  16192  mhmco  16195  gasubg  16542  idrespermg  16638  rhmco  17584  resrhm  17656  cply1mul  18533  dmatmul  19169  scmatf1  19203  slesolinv  19352  slesolinvbi  19353  slesolex  19354  cramerimplem3  19357  cramerimp  19358  chfacfscmulgsum  19531  chfacfpmmulgsum  19535  bwth  20080  nmhmco  21432  chpchtsum  23695  dchrisum0lem1  23902  wlkdvspthlem  24814  clwlkisclwwlklem0  24993  clwwlkf1  25001  wwlksubclwwlk  25009  clwlkfclwwlk  25049  clwlkf1clwwlklem  25054  vdgrf  25103  frgra3v  25207  frgrancvvdeqlem3  25237  frghash2spot  25268  numclwwlk3  25314  numclwwlk5  25317  frgrareg  25322  occon2  26407  itgspltprt  32020  2rexreu  32432  nn0e  32611  resmgmhm  32877  mgmhmco  32880  rnghmco  32986  ztprmneprm  33209  nn0sumltlt  33212  ldepspr  33347  m1modmmod  33407  blennngt2o2  33486  aacllem  33623  bnj1110  34458
  Copyright terms: Public domain W3C validator