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  9433  fzolb  13824  brfi1uzind  14677  opfi1uzind  14680  01sqrexlem5  15439  bitsmod  16632  isfunc  18065  txcn  23972  trfil2  24233  isclmp  25445  eulerpartlemn  35080  bnj976  35475  bnj543  35590  bnj594  35609  bnj917  35631  topdifinffinlem  38461  dath  40984  oeord2com  44503  ichexmpl1  48754  grtriproplem  49240  grtrif1o  49243  elfzolborelfzop1  49834  nnolog2flm1  49905  isthincd2  50775