Theorem 3anim1i 1148

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl3an1  1159  syl3anl1  1408  syl3anr1  1412  fnsuppres  7857  elfiun  8894  elioc2  12800  elico2  12801  elicc2  12802  dvdsleabs2  15662  cphipval  23846  spthonpthon  27532  uhgrwkspth  27536  usgr2wlkspth  27540  upgriseupth  27986  cm2j  29397  bnj544  32166  btwnconn1lem4  33551  relowlssretop  34647  dalem53  36876  dalem54  36877  paddasslem14  36984  mzpcong  39589  itscnhlc0xyqsol  44772