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

Theorem anim12ci 567
Description: Variant of anim12i 566 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 566 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 453 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  2exeu  2380  dfco2a  5507  fliftval  6203  omlimcl  7228  funsnfsupp  7854  supmaxlem  7925  ltrnq  9358  ltsrpr  9455  difelfznle  11787  swrdspsleq  12639  swrdccatin12lem2a  12676  repswswrd  12722  cshwidxm  12744  modprm0  14192  brssc  15047  resmhm  15812  mhmco  15815  gasubg  16154  idrespermg  16250  rhmco  17198  resrhm  17270  cply1mul  18146  dmatmul  18806  scmatf1  18840  slesolinv  18989  slesolinvbi  18990  slesolex  18991  cramerimplem3  18994  cramerimp  18995  chfacfscmulgsum  19168  chfacfpmmulgsum  19172  bwth  19716  nmhmco  21090  chpchtsum  23319  dchrisum0lem1  23526  wlkdvspthlem  24382  clwlkisclwwlklem0  24561  clwwlkf1  24569  wwlksubclwwlk  24577  clwlkfclwwlk  24617  clwlkf1clwwlklem  24622  vdgrf  24671  frgra3v  24775  frgrancvvdeqlem3  24806  frghash2spot  24837  numclwwlk3  24883  numclwwlk5  24886  frgrareg  24891  occon2  25979  icccncfext  31453  cncfiooicclem1  31459  iblspltprt  31518  itgspltprt  31524  2rexreu  31884  ztprmneprm  32231  nn0sumltlt  32234  ldepspr  32372  bnj1110  33334
  Copyright terms: Public domain W3C validator