Theorem 3anim1i 1170

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 23	. 2 ⊢ (𝜒 → 𝜒)
3		id 23	. 2 ⊢ (𝜃 → 𝜃)
4	1, 2, 3	3anim123i 1169	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  syl3an1  1181  syl3anl1  1439  syl3anr1  1443  fnsuppres  8183  dif1en  9142  elfiun  9386  elioc2  13431  elico2  13432  elicc2  13433  dvdsleabs2  16365  subrngringnsg  20652  cphipval  25402  spthonpthon  30100  uhgrwkspth  30104  usgr2wlkspth  30108  upgriseupth  30558  cm2j  31972  bnj544  35282  btwnconn1lem4  36582  relowlssretop  38029  dalem53  40519  dalem54  40520  paddasslem14  40627  mzpcong  43719  itscnhlc0xyqsol  49565