Theorem 3anim1i 1170

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 23	. 2 ⊢ (𝜒 → 𝜒)
3		id 23	. 2 ⊢ (𝜃 → 𝜃)
4	1, 2, 3	3anim123i 1169	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl3an1  1181  syl3anl1  1439  syl3anr1  1443  fnsuppres  8219  dif1en  9188  elfiun  9432  elioc2  13550  elico2  13551  elicc2  13552  dvdsleabs2  16494  dfring2  20529  subrngringnsg  20817  cphipval  25576  spthonpthon  30349  uhgrwkspth  30353  usgr2wlkspth  30357  upgriseupth  30820  cm2j  32234  bnj544  35577  btwnconn1lem4  36982  relowlssretop  38426  dalem53  40922  dalem54  40923  paddasslem14  41030  mzpcong  44119  itscnhlc0xyqsol  50016