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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl3an1  1162  syl3anl1  1411  syl3anr1  1415  fnsuppres  8007  elfiun  9189  elioc2  13142  elico2  13143  elicc2  13144  dvdsleabs2  16021  cphipval  24407  spthonpthon  28119  uhgrwkspth  28123  usgr2wlkspth  28127  upgriseupth  28571  cm2j  29982  bnj544  32874  btwnconn1lem4  34392  relowlssretop  35534  dalem53  37739  dalem54  37740  paddasslem14  37847  mzpcong  40794  itscnhlc0xyqsol  46111