Theorem 3anim1i 1158

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 1157	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl3an1  1169  syl3anl1  1420  syl3anr1  1424  fnsuppres  8131  dif1en  9086  elfiun  9333  elioc2  13353  elico2  13354  elicc2  13355  dvdsleabs2  16272  subrngringnsg  20525  cphipval  25228  spthonpthon  29837  uhgrwkspth  29841  usgr2wlkspth  29845  upgriseupth  30295  cm2j  31709  bnj544  35076  btwnconn1lem4  36318  relowlssretop  37725  dalem53  40217  dalem54  40218  paddasslem14  40325  mzpcong  43417  itscnhlc0xyqsol  49256