Theorem 3anbi1i 1154

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

Syntax hints:   ↔ wb 205   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  iinfi  9461  fzolb  13696  brfi1uzind  14530  opfi1uzind  14533  01sqrexlem5  15264  bitsmod  16449  isfunc  17896  txcn  23621  trfil2  23882  isclmp  25115  eulerpartlemn  34291  bnj976  34698  bnj543  34814  bnj594  34833  bnj917  34855  topdifinffinlem  37139  dath  39520  oeord2com  43089  ichexmpl1  47152  grtriproplem  47623  grtrif1o  47626  elfzolborelfzop1  48024  nnolog2flm1  48100  isthincd2  48481