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  9387  fzolb  13754  brfi1uzind  14606  opfi1uzind  14609  01sqrexlem5  15366  bitsmod  16559  isfunc  17986  txcn  23892  trfil2  24153  isclmp  25365  eulerpartlemn  34933  bnj976  35328  bnj543  35443  bnj594  35462  bnj917  35484  topdifinffinlem  38184  dath  40707  oeord2com  44250  ichexmpl1  48467  grtriproplem  48953  grtrif1o  48956  elfzolborelfzop1  49547  nnolog2flm1  49618  isthincd2  50461