Theorem 3anim1i 1153

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 1152	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  1164  syl3anl1  1415  syl3anr1  1419  fnsuppres  8141  dif1en  9096  elfiun  9343  elioc2  13362  elico2  13363  elicc2  13364  dvdsleabs2  16281  subrngringnsg  20530  cphipval  25210  spthonpthon  29819  uhgrwkspth  29823  usgr2wlkspth  29827  upgriseupth  30277  cm2j  31691  bnj544  35036  btwnconn1lem4  36272  relowlssretop  37679  dalem53  40171  dalem54  40172  paddasslem14  40279  mzpcong  43400  itscnhlc0xyqsol  49241