Theorem 3anim1i 1165

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

Hypothesis

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

Assertion

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

Proof of Theorem 3anim1i

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

Syntax hints:   → wi 4   ∧ w3a 1098

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 400  df-3an 1100

This theorem is referenced by:  syl3an1  1176  syl3anl1  1431  syl3anr1  1435  fnsuppres  8171  dif1en  9130  elfiun  9376  elioc2  13413  elico2  13414  elicc2  13415  dvdsleabs2  16346  subrngringnsg  20603  cphipval  25305  spthonpthon  29951  uhgrwkspth  29955  usgr2wlkspth  29959  upgriseupth  30409  cm2j  31823  bnj544  35189  btwnconn1lem4  36440  relowlssretop  37857  dalem53  40349  dalem54  40350  paddasslem14  40457  mzpcong  43549  itscnhlc0xyqsol  49387