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 210  df-an 400  df-3an 1086

This theorem is referenced by:  syl3an1  1160  syl3anl1  1409  syl3anr1  1413  fnsuppres  7840  elfiun  8878  elioc2  12788  elico2  12789  elicc2  12790  dvdsleabs2  15654  cphipval  23847  spthonpthon  27540  uhgrwkspth  27544  usgr2wlkspth  27548  upgriseupth  27992  cm2j  29403  bnj544  32276  btwnconn1lem4  33664  relowlssretop  34780  dalem53  37021  dalem54  37022  paddasslem14  37129  mzpcong  39913  itscnhlc0xyqsol  45179