Theorem 3anim3i 1161

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  syl3an3  1172  syl3anl3  1423  syl3anr3  1427  elioo4g  13354  ssnn0fi  13942  tmdcn2  24076  axcont  29067  numclwwlk3  30477  minvecolem3  30969  bnj556  35097  bnj557  35098  bnj1145  35190  btwnconn1lem4  36333  btwnconn1lem5  36334  btwnconn1lem6  36335  bj-ceqsalt  37254  bj-ceqsaltv  37255  uhgrimisgrgric  48436  clnbgr3stgrgrlim  48524