Theorem anim12ci 339

Description: Variant of anim12i 338 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

Step	Hyp	Ref	Expression
1		anim12i.2	. . 3 |- ( ch -> th )
2		anim12i.1	. . 3 |- ( ph -> ps )
3	1, 2	anim12i 338	. 2 |- ( ( ch /\ ph ) -> ( th /\ ps ) )
4	3	ancoms 268	1 |- ( ( ph /\ ch ) -> ( th /\ ps ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anim1ci  341  dfco2a  5291  funco  5420  fliftval  6009  ltsrprg  8120  difelfznle  10558  nelfzo  10575  iseqf1olemqk  10964  ccatsymb  11391  pfxsuffeqwrdeq  11491  pfxccatin12lem2a  11520  difsqpwdvds  13145  resmhm  13852  mhmco  13855  rhmco  14589  resrhm  14664  gausslemma2dlem1a  16399  subusgr  16738  ex-ceil  16962