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  9458  fzolb  13706  brfi1uzind  14548  opfi1uzind  14551  01sqrexlem5  15286  bitsmod  16474  isfunc  17910  txcn  23635  trfil2  23896  isclmp  25131  eulerpartlemn  34384  bnj976  34792  bnj543  34908  bnj594  34927  bnj917  34949  topdifinffinlem  37349  dath  39739  oeord2com  43329  ichexmpl1  47461  grtriproplem  47911  grtrif1o  47914  elfzolborelfzop1  48441  nnolog2flm1  48516  isthincd2  49111