Theorem 3anim1i 1152

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  syl3an1  1163  syl3anl1  1414  syl3anr1  1418  fnsuppres  8173  dif1en  9130  elfiun  9388  elioc2  13377  elico2  13378  elicc2  13379  dvdsleabs2  16289  subrngringnsg  20469  cphipval  25150  spthonpthon  29688  uhgrwkspth  29692  usgr2wlkspth  29696  upgriseupth  30143  cm2j  31556  bnj544  34891  btwnconn1lem4  36085  relowlssretop  37358  dalem53  39726  dalem54  39727  paddasslem14  39834  mzpcong  42968  itscnhlc0xyqsol  48758