Theorem 3anim3i 1153

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl3an3  1164  syl3anl3  1413  syl3anr3  1417  elioo4g  13443  ssnn0fi  14022  tmdcn2  24112  axcont  29005  numclwwlk3  30413  minvecolem3  30904  bnj556  34892  bnj557  34893  bnj1145  34985  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  bj-ceqsalt  36868  bj-ceqsaltv  36869  uhgrimisgrgric  47836