Theorem 3anim1i 1241

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl3an1  1351  syl3anl1  1366  syl3anr1  1370  fnsuppres  7209  elfiun  8219  elioc2  12107  elico2  12108  elicc2  12109  dvdsleabs2  14872  mulgnndir  17392  mulgnnass  17399  cphipval  22850  trliswlk  26069  isspthonpth  26114  usg2wotspth  26411  cm2j  27863  bnj544  30218  btwnconn1lem4  31367  relowlssretop  32387  dalem53  34029  dalem54  34030  paddasslem14  34137  mzpcong  36557  spthonpthon  40957  uhgr1wlkspth  40961  usgr2wlkspth  40965  upgriseupth  41375