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  2220  dfco2a  5173  fliftval  5815  omlimcl  6576  supmaxlem  7215  ltrnq  8603  ltsrpr  8699  brssc  13691  resmhm  14436  mhmco  14439  gasubg  14756  rhmco  15509  resrhm  15574  nmhmco  18265  chpchtsum  20458  dchrisum0lem1  20665  occon2  21867  clscnc  26010  2rexreu  27963  frgra3v  28180  bnj1110  29012
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