Theorem 3anim1i 1168

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 1167	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl3an1  1179  syl3anl1  1437  syl3anr1  1441  fnsuppres  8187  dif1en  9146  elfiun  9390  elioc2  13436  elico2  13437  elicc2  13438  dvdsleabs2  16370  subrngringnsg  20638  cphipval  25371  spthonpthon  30041  uhgrwkspth  30045  usgr2wlkspth  30049  upgriseupth  30499  cm2j  31913  bnj544  35227  btwnconn1lem4  36481  relowlssretop  37897  dalem53  40389  dalem54  40390  paddasslem14  40497  mzpcong  43591  itscnhlc0xyqsol  49430