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  5225  funco  5354  fliftval  5917  ltsrprg  7922  difelfznle  10319  nelfzo  10336  iseqf1olemqk  10716  ccatsymb  11123  pfxsuffeqwrdeq  11216  pfxccatin12lem2a  11245  difsqpwdvds  12847  resmhm  13506  mhmco  13509  rhmco  14123  resrhm  14197  gausslemma2dlem1a  15722  ex-ceil  16020