Theorem 3anim1i 1170

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 23	. 2 ⊢ (𝜒 → 𝜒)
3		id 23	. 2 ⊢ (𝜃 → 𝜃)
4	1, 2, 3	3anim123i 1169	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl3an1  1181  syl3anl1  1440  syl3anr1  1444  fnsuppres  8246  dif1en  9215  elfiun  9459  elioc2  13580  elico2  13581  elicc2  13582  dvdsleabs2  16526  dfring2  20568  subrngringnsg  20856  cphipval  25619  spthonpthon  30394  uhgrwkspth  30398  usgr2wlkspth  30402  upgriseupth  30865  cm2j  32279  bnj544  35635  btwnconn1lem4  37070  relowlssretop  38554  dalem53  41048  dalem54  41049  paddasslem14  41156  mzpcong  44245  itscnhlc0xyqsol  50208