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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  iinfi  9408  fzolb  13634  brfi1uzind  14455  opfi1uzind  14458  01sqrexlem5  15189  bitsmod  16373  isfunc  17810  txcn  23121  trfil2  23382  isclmp  24604  eulerpartlemn  33368  bnj976  33776  bnj543  33892  bnj594  33911  bnj917  33933  topdifinffinlem  36216  dath  38595  oeord2com  42046  ichexmpl1  46123  elfzolborelfzop1  47153  nnolog2flm1  47229  isthincd2  47611