Theorem 3anim1i 1152

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl3an1  1163  syl3anl1  1412  syl3anr1  1416  fnsuppres  8127  dif1en  9111  elfiun  9375  elioc2  13337  elico2  13338  elicc2  13339  dvdsleabs2  16205  cphipval  24644  spthonpthon  28762  uhgrwkspth  28766  usgr2wlkspth  28770  upgriseupth  29214  cm2j  30625  bnj544  33595  btwnconn1lem4  34751  relowlssretop  35907  dalem53  38261  dalem54  38262  paddasslem14  38369  mzpcong  41354  itscnhlc0xyqsol  46971