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  9365  fzolb  13682  brfi1uzind  14533  opfi1uzind  14536  01sqrexlem5  15285  bitsmod  16482  isfunc  17909  txcn  23740  trfil2  24001  isclmp  25213  eulerpartlemn  34683  bnj976  35078  bnj543  35193  bnj594  35212  bnj917  35234  topdifinffinlem  37848  dath  40367  oeord2com  43895  ichexmpl1  48074  grtriproplem  48560  grtrif1o  48563  elfzolborelfzop1  49151  nnolog2flm1  49222  isthincd2  50067