Theorem 3anim1i 1151

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 1150	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  1162  syl3anl1  1411  syl3anr1  1415  fnsuppres  8215  dif1en  9199  elfiun  9468  elioc2  13447  elico2  13448  elicc2  13449  dvdsleabs2  16346  subrngringnsg  20570  cphipval  25291  spthonpthon  29784  uhgrwkspth  29788  usgr2wlkspth  29792  upgriseupth  30236  cm2j  31649  bnj544  34887  btwnconn1lem4  36072  relowlssretop  37346  dalem53  39708  dalem54  39709  paddasslem14  39816  mzpcong  42961  itscnhlc0xyqsol  48615