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

Theorem anim12ci 552
Description: Variant of anim12i 551 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 551 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 441 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  2exeu  2359  dfco2a  5371  fliftval  6039  omlimcl  6822  supmaxlem  7470  ltrnq  8857  ltsrpr  8953  brssc  14015  resmhm  14760  mhmco  14763  gasubg  15080  rhmco  15833  resrhm  15898  nmhmco  18791  chpchtsum  21004  dchrisum0lem1  21211  wlkdvspthlem  21608  vdgrf  21670  occon2  22791  2rexreu  27940  swrdccatin12lem3a  28209  modprm0  28229  cshwidxmod  28244  2cshw1lem1  28249  2cshw2lem2  28254  2cshwmod  28258  frgra3v  28393  frgrancvvdeqlem3  28422  frghash2spot  28453  bnj1110  29352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator