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  8135  dif1en  9090  elfiun  9337  elioc2  13356  elico2  13357  elicc2  13358  dvdsleabs2  16275  subrngringnsg  20524  cphipval  25223  spthonpthon  29837  uhgrwkspth  29841  usgr2wlkspth  29845  upgriseupth  30295  cm2j  31709  bnj544  35055  btwnconn1lem4  36291  relowlssretop  37696  dalem53  40188  dalem54  40189  paddasslem14  40296  mzpcong  43421  itscnhlc0xyqsol  49256