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  9344  fzolb  13602  brfi1uzind  14449  opfi1uzind  14452  01sqrexlem5  15188  bitsmod  16382  isfunc  17802  txcn  23489  trfil2  23750  isclmp  24973  eulerpartlemn  34345  bnj976  34740  bnj543  34856  bnj594  34875  bnj917  34897  topdifinffinlem  37308  dath  39703  oeord2com  43273  ichexmpl1  47443  grtriproplem  47911  grtrif1o  47914  elfzolborelfzop1  48481  nnolog2flm1  48552  isthincd2  49399