Theorem 3anbi1i 1158

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 261	. 2 ⊢ (𝜒 ↔ 𝜒)
3		biid 261	. 2 ⊢ (𝜃 ↔ 𝜃)
4	1, 2, 3	3anbi123i 1156	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  iinfi  9332  fzolb  13593  brfi1uzind  14443  opfi1uzind  14446  01sqrexlem5  15181  bitsmod  16375  isfunc  17800  txcn  23582  trfil2  23843  isclmp  25065  eulerpartlemn  34559  bnj976  34954  bnj543  35069  bnj594  35088  bnj917  35110  topdifinffinlem  37602  dath  40112  oeord2com  43668  ichexmpl1  47829  grtriproplem  48299  grtrif1o  48302  elfzolborelfzop1  48879  nnolog2flm1  48950  isthincd2  49796