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

This theorem is referenced by:  syl3an1  1161  syl3anl1  1410  syl3anr1  1414  fnsuppres  8178  dif1en  9162  elfiun  9427  elioc2  13391  elico2  13392  elicc2  13393  dvdsleabs2  16259  subrngringnsg  20441  cphipval  24991  spthonpthon  29275  uhgrwkspth  29279  usgr2wlkspth  29283  upgriseupth  29727  cm2j  31140  bnj544  34203  btwnconn1lem4  35366  relowlssretop  36547  dalem53  38899  dalem54  38900  paddasslem14  39007  mzpcong  42013  itscnhlc0xyqsol  47538