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  8208  dif1en  9177  elfiun  9422  elioc2  13540  elico2  13541  elicc2  13542  dvdsleabs2  16482  dfring2  20517  subrngringnsg  20805  cphipval  25564  spthonpthon  30337  uhgrwkspth  30341  usgr2wlkspth  30345  upgriseupth  30808  cm2j  32222  bnj544  35524  btwnconn1lem4  36855  relowlssretop  38286  dalem53  40782  dalem54  40783  paddasslem14  40890  mzpcong  43978  itscnhlc0xyqsol  49876