Theorem 3anbi1i 1173

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

Syntax hints:   ↔ wb 209   ∧ w3a 1101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  iinfi  9377  fzolb  13694  brfi1uzind  14545  opfi1uzind  14548  01sqrexlem5  15297  bitsmod  16494  isfunc  17921  txcn  23752  trfil2  24013  isclmp  25225  eulerpartlemn  34716  bnj976  35111  bnj543  35226  bnj594  35245  bnj917  35267  topdifinffinlem  37916  dath  40435  oeord2com  43965  ichexmpl1  48142  grtriproplem  48628  grtrif1o  48631  elfzolborelfzop1  49219  nnolog2flm1  49290  isthincd2  50135