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  8133  dif1en  9086  elfiun  9333  elioc2  13325  elico2  13326  elicc2  13327  dvdsleabs2  16239  subrngringnsg  20486  cphipval  25199  spthonpthon  29824  uhgrwkspth  29828  usgr2wlkspth  29832  upgriseupth  30282  cm2j  31695  bnj544  35050  btwnconn1lem4  36284  relowlssretop  37568  dalem53  39995  dalem54  39996  paddasslem14  40103  mzpcong  43224  itscnhlc0xyqsol  49021