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 ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anim1ci  341  dfco2a  5189  funco  5317  fliftval  5879  ltsrprg  7873  difelfznle  10270  nelfzo  10287  iseqf1olemqk  10665  ccatsymb  11072  pfxsuffeqwrdeq  11163  difsqpwdvds  12711  resmhm  13369  mhmco  13372  rhmco  13986  resrhm  14060  gausslemma2dlem1a  15585  ex-ceil  15776