Theorem 3anbi1i 1175

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

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

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 402  df-3an 1105

This theorem is used by:  iinfi  9390  fzolb  13723  brfi1uzind  14575  opfi1uzind  14578  01sqrexlem5  15335  bitsmod  16530  isfunc  17957  txcn  23853  trfil2  24114  isclmp  25326  eulerpartlemn  34879  bnj976  35274  bnj543  35389  bnj594  35408  bnj917  35430  topdifinffinlem  38088  dath  40596  oeord2com  44139  ichexmpl1  48356  grtriproplem  48842  grtrif1o  48845  elfzolborelfzop1  49436  nnolog2flm1  49507  isthincd2  50350