Theorem 3anbi1i 1156

Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
3anbi1i	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Proof of Theorem 3anbi1i

Step	Hyp	Ref	Expression
1		3anbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		biid 260	. 2 ⊢ (𝜒 ↔ 𝜒)
3		biid 260	. 2 ⊢ (𝜃 ↔ 𝜃)
4	1, 2, 3	3anbi123i 1154	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   ↔ wb 205   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  iinfi  9176  fzolb  13393  brfi1uzind  14212  opfi1uzind  14215  sqrlem5  14958  bitsmod  16143  isfunc  17579  txcn  22777  trfil2  23038  isclmp  24260  eulerpartlemn  32348  bnj976  32757  bnj543  32873  bnj594  32892  bnj917  32914  topdifinffinlem  35518  dath  37750  ichexmpl1  44921  elfzolborelfzop1  45860  nnolog2flm1  45936  isthincd2  46319