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

Theorem anim12ci 569
Description: Variant of anim12i 568 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 568 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 454 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  2exeu  2355  dfco2a  5297  fliftval  6168  omlimcl  7234  funsnfsupp  7860  supmaxlemOLD  7935  ltrnq  9355  ltsrpr  9452  difelfznle  11856  nelfzo  11876  muladdmodid  12087  hash2prd  12582  swrdccatin12lem2a  12787  repswswrd  12833  cshwidxm  12855  lcmftp  14552  ncoprmlnprm  14620  modprm0  14699  brssc  15662  resmhm  16549  mhmco  16552  gasubg  16899  idrespermg  16995  rhmco  17908  resrhm  17980  cply1mul  18830  dmatmul  19464  scmatf1  19498  slesolinv  19647  slesolinvbi  19648  slesolex  19649  cramerimplem3  19652  cramerimp  19653  chfacfscmulgsum  19826  chfacfpmmulgsum  19830  bwth  20367  nmhmco  21719  chpchtsum  24089  dchrisum0lem1  24296  wlkdvspthlem  25279  clwlkisclwwlklem0  25458  clwwlkf1  25466  wwlksubclwwlk  25474  clwlkfclwwlk  25514  clwlkf1clwwlklem  25519  vdgrf  25568  frgra3v  25672  frgrancvvdeqlem3  25702  frghash2spot  25733  numclwwlk3  25779  numclwwlk5  25782  frgrareg  25787  occon2  26883  bnj1110  29743  relowlssretop  31673  poimirlem16  31863  poimirlem19  31866  poimirlem30  31877  itgspltprt  37739  2rexreu  38420  iccpartiltu  38549  iccpartgt  38554  nn0e  38639  stgoldbwt  38690  bgoldbtbndlem3  38715  bgoldbtbndlem4  38716  bgoldbtbnd  38717  subusgr  39108  isuvtxa  39207  iscplgredg  39223  resmgmhm  39399  mgmhmco  39402  rnghmco  39508  ztprmneprm  39731  nn0sumltlt  39734  ldepspr  39869  m1modmmod  39927  blennngt2o2  40006  aacllem  40143
  Copyright terms: Public domain W3C validator