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  8190  dif1en  9159  elfiun  9403  elioc2  13465  elico2  13466  elicc2  13467  dvdsleabs2  16405  dfring2  20432  subrngringnsg  20718  cphipval  25474  spthonpthon  30219  uhgrwkspth  30223  usgr2wlkspth  30227  upgriseupth  30690  cm2j  32104  bnj544  35406  btwnconn1lem4  36673  relowlssretop  38120  dalem53  40601  dalem54  40602  paddasslem14  40709  mzpcong  43816  itscnhlc0xyqsol  49698