Theorem 3anbi1i 1155

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

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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

This theorem is referenced by:  iinfi  9106  fzolb  13322  brfi1uzind  14140  opfi1uzind  14143  sqrlem5  14886  bitsmod  16071  isfunc  17495  txcn  22685  trfil2  22946  isclmp  24166  eulerpartlemn  32248  bnj976  32657  bnj543  32773  bnj594  32792  bnj917  32814  topdifinffinlem  35445  dath  37677  ichexmpl1  44809  elfzolborelfzop1  45748  nnolog2flm1  45824  isthincd2  46207