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  2358  dfco2a  5338  fliftval  6009  omlimcl  7017  funsnfsupp  7644  supmaxlem  7714  ltrnq  9148  ltsrpr  9244  swrdspsleq  12342  swrdccatin12lem2a  12376  repswswrd  12422  cshwidxm  12444  modprm0  13873  brssc  14727  resmhm  15487  mhmco  15490  gasubg  15820  idrespermg  15916  rhmco  16825  resrhm  16894  slesolinv  18486  slesolinvbi  18487  slesolex  18488  cramerimplem3  18491  cramerimp  18492  bwth  19013  nmhmco  20335  chpchtsum  22558  dchrisum0lem1  22765  wlkdvspthlem  23506  vdgrf  23568  occon2  24691  2rexreu  30009  clwlkisclwwlklem0  30450  clwwlkf1  30458  wwlksubclwwlk  30466  difelfznle  30488  clwlkfclwwlk  30517  clwlkf1clwwlklem  30522  frgra3v  30594  frgrancvvdeqlem3  30625  frghash2spot  30656  numclwwlk3  30702  numclwwlk5  30705  frgrareg  30710  ztprmneprm  30739  nn0sumltlt  30742  dmatmul  30876  ldepspr  31007  bnj1110  31973
  Copyright terms: Public domain W3C validator