Theorem 3anbi1i 1157

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  iinfi  9434  fzolb  13687  brfi1uzind  14531  opfi1uzind  14534  01sqrexlem5  15270  bitsmod  16460  isfunc  17882  txcn  23569  trfil2  23830  isclmp  25053  eulerpartlemn  34418  bnj976  34813  bnj543  34929  bnj594  34948  bnj917  34970  topdifinffinlem  37370  dath  39760  oeord2com  43302  ichexmpl1  47450  grtriproplem  47918  grtrif1o  47921  elfzolborelfzop1  48462  nnolog2flm1  48537  isthincd2  49290