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  1414  syl3anr1  1418  fnsuppres  8216  dif1en  9200  elfiun  9470  elioc2  13450  elico2  13451  elicc2  13452  dvdsleabs2  16349  subrngringnsg  20553  cphipval  25277  spthonpthon  29771  uhgrwkspth  29775  usgr2wlkspth  29779  upgriseupth  30226  cm2j  31639  bnj544  34908  btwnconn1lem4  36091  relowlssretop  37364  dalem53  39727  dalem54  39728  paddasslem14  39835  mzpcong  42984  itscnhlc0xyqsol  48686