Theorem 3anim1i 1168

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  syl3an1  1179  syl3anl1  1437  syl3anr1  1441  fnsuppres  8186  dif1en  9145  elfiun  9389  elioc2  13435  elico2  13436  elicc2  13437  dvdsleabs2  16369  subrngringnsg  20637  cphipval  25370  spthonpthon  30040  uhgrwkspth  30044  usgr2wlkspth  30048  upgriseupth  30498  cm2j  31912  bnj544  35226  btwnconn1lem4  36480  relowlssretop  37896  dalem53  40388  dalem54  40389  paddasslem14  40496  mzpcong  43590  itscnhlc0xyqsol  49429