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  1439  syl3anr1  1443  fnsuppres  8193  dif1en  9153  elfiun  9397  elioc2  13454  elico2  13455  elicc2  13456  dvdsleabs2  16394  dfring2  20418  subrngringnsg  20704  cphipval  25455  spthonpthon  30166  uhgrwkspth  30170  usgr2wlkspth  30174  upgriseupth  30631  cm2j  32045  bnj544  35349  btwnconn1lem4  36621  relowlssretop  38068  dalem53  40559  dalem54  40560  paddasslem14  40667  mzpcong  43759  itscnhlc0xyqsol  49604