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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl3an1  1163  syl3anl1  1412  syl3anr1  1416  fnsuppres  8232  dif1en  9226  elfiun  9499  elioc2  13470  elico2  13471  elicc2  13472  dvdsleabs2  16360  subrngringnsg  20579  cphipval  25296  spthonpthon  29787  uhgrwkspth  29791  usgr2wlkspth  29795  upgriseupth  30239  cm2j  31652  bnj544  34870  btwnconn1lem4  36054  relowlssretop  37329  dalem53  39682  dalem54  39683  paddasslem14  39790  mzpcong  42929  itscnhlc0xyqsol  48499