Theorem anim12ci 339

Description: Variant of anim12i 338 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
anim12i.1	⊢ (𝜑 → 𝜓)
anim12i.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
anim12ci	⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Proof of Theorem anim12ci

Step	Hyp	Ref	Expression
1		anim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
2		anim12i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 338	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜃 ∧ 𝜓))
4	3	ancoms 268	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

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  5288  funco  5417  fliftval  6006  ltsrprg  8114  difelfznle  10544  nelfzo  10561  iseqf1olemqk  10946  ccatsymb  11372  pfxsuffeqwrdeq  11472  pfxccatin12lem2a  11501  difsqpwdvds  13119  resmhm  13796  mhmco  13799  rhmco  14483  resrhm  14558  gausslemma2dlem1a  16189  subusgr  16528  ex-ceil  16752