Theorem 3anim1i 1149

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 1086

This theorem is referenced by:  syl3an1  1160  syl3anl1  1409  syl3anr1  1413  fnsuppres  8194  dif1en  9187  elfiun  9463  elioc2  13432  elico2  13433  elicc2  13434  dvdsleabs2  16306  subrngringnsg  20528  cphipval  25256  spthonpthon  29682  uhgrwkspth  29686  usgr2wlkspth  29690  upgriseupth  30134  cm2j  31547  bnj544  34749  btwnconn1lem4  35924  relowlssretop  37080  dalem53  39434  dalem54  39435  paddasslem14  39542  mzpcong  42664  itscnhlc0xyqsol  48186