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  9409  fzolb  13800  brfi1uzind  14653  opfi1uzind  14656  01sqrexlem5  15413  bitsmod  16606  isfunc  18039  txcn  23945  trfil2  24206  isclmp  25418  eulerpartlemn  35013  bnj976  35408  bnj543  35523  bnj594  35542  bnj917  35564  topdifinffinlem  38271  dath  40794  oeord2com  44313  ichexmpl1  48551  grtriproplem  49037  grtrif1o  49040  elfzolborelfzop1  49631  nnolog2flm1  49702  isthincd2  50545