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

Theorem anim12ci 550
Description: Variant of anim12i 549 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 549 . 2  |-  ( ( ch  /\  ph )  ->  ( th  /\  ps ) )
43ancoms 439 1  |-  ( (
ph  /\  ch )  ->  ( th  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  2exeu  2233  dfco2a  5189  fliftval  5831  omlimcl  6592  supmaxlem  7231  ltrnq  8619  ltsrpr  8715  brssc  13707  resmhm  14452  mhmco  14455  gasubg  14772  rhmco  15525  resrhm  15590  nmhmco  18281  chpchtsum  20474  dchrisum0lem1  20681  occon2  21883  clscnc  26113  2rexreu  28066  wlkdvspthlem  28365  frgra3v  28426  bnj1110  29328
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 177  df-an 360
  Copyright terms: Public domain W3C validator