Theorem 3anbi1i 1157

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

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  iinfi  9320  fzolb  13581  brfi1uzind  14431  opfi1uzind  14434  01sqrexlem5  15169  bitsmod  16363  isfunc  17788  txcn  23570  trfil2  23831  isclmp  25053  eulerpartlemn  34538  bnj976  34933  bnj543  35049  bnj594  35068  bnj917  35090  topdifinffinlem  37552  dath  40006  oeord2com  43563  ichexmpl1  47725  grtriproplem  48195  grtrif1o  48198  elfzolborelfzop1  48775  nnolog2flm1  48846  isthincd2  49692