Theorem 3anbi1i 1158

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 261	. 2 ⊢ (𝜒 ↔ 𝜒)
3		biid 261	. 2 ⊢ (𝜃 ↔ 𝜃)
4	1, 2, 3	3anbi123i 1156	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  iinfi  9330  fzolb  13620  brfi1uzind  14470  opfi1uzind  14473  01sqrexlem5  15208  bitsmod  16405  isfunc  17831  txcn  23591  trfil2  23852  isclmp  25064  eulerpartlemn  34525  bnj976  34920  bnj543  35035  bnj594  35054  bnj917  35076  topdifinffinlem  37663  dath  40182  oeord2com  43739  ichexmpl1  47929  grtriproplem  48415  grtrif1o  48418  elfzolborelfzop1  48995  nnolog2flm1  49066  isthincd2  49912