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  7996  elfiun  9165  elioc2  13139  elico2  13140  elicc2  13141  dvdsleabs2  16017  cphipval  24403  spthonpthon  28113  uhgrwkspth  28117  usgr2wlkspth  28121  upgriseupth  28565  cm2j  29976  bnj544  32868  btwnconn1lem4  34386  relowlssretop  35528  dalem53  37733  dalem54  37734  paddasslem14  37841  mzpcong  40789  itscnhlc0xyqsol  46078