Theorem 3anim3i 1243

Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypothesis

Ref	Expression
3animi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3anim3i	⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Proof of Theorem 3anim3i

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜒 → 𝜒)
2		id 22	. 2 ⊢ (𝜃 → 𝜃)
3		3animi.1	. 2 ⊢ (𝜑 → 𝜓)
4	1, 2, 3	3anim123i 1240	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl3anl3  1368  syl3anr3  1372  elioo4g  12105  ssnn0fi  12646  tmdcn2  21703  axcont  25656  constr3lem4  26175  extwwlkfab  26617  minvecolem3  27116  bnj556  30224  bnj557  30225  bnj1145  30315  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  bj-ceqsalt  32069  bj-ceqsaltv  32070  1ewlk  41283  1pthon2ve  41321  av-numclwwlk3  41539