Theorem 3anim1i 1150

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl3an1  1161  syl3anl1  1410  syl3anr1  1414  fnsuppres  7978  elfiun  9119  elioc2  13071  elico2  13072  elicc2  13073  dvdsleabs2  15949  cphipval  24312  spthonpthon  28020  uhgrwkspth  28024  usgr2wlkspth  28028  upgriseupth  28472  cm2j  29883  bnj544  32774  btwnconn1lem4  34319  relowlssretop  35461  dalem53  37666  dalem54  37667  paddasslem14  37774  mzpcong  40710  itscnhlc0xyqsol  45999