Theorem 3anbi1i 1174

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  iinfi  9375  fzolb  13701  brfi1uzind  14552  opfi1uzind  14555  01sqrexlem5  15304  bitsmod  16500  isfunc  17927  txcn  23794  trfil2  24055  isclmp  25267  eulerpartlemn  34780  bnj976  35175  bnj543  35290  bnj594  35309  bnj917  35331  topdifinffinlem  38021  dath  40538  oeord2com  44066  ichexmpl1  48246  grtriproplem  48732  grtrif1o  48735  elfzolborelfzop1  49327  nnolog2flm1  49398  isthincd2  50243