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  8143  dif1en  9098  elfiun  9345  elioc2  13337  elico2  13338  elicc2  13339  dvdsleabs2  16251  subrngringnsg  20498  cphipval  25211  spthonpthon  29836  uhgrwkspth  29840  usgr2wlkspth  29844  upgriseupth  30294  cm2j  31708  bnj544  35070  btwnconn1lem4  36306  relowlssretop  37618  dalem53  40101  dalem54  40102  paddasslem14  40209  mzpcong  43329  itscnhlc0xyqsol  49125