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 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  9486  fzolb  13722  brfi1uzind  14557  opfi1uzind  14560  01sqrexlem5  15295  bitsmod  16482  isfunc  17928  txcn  23655  trfil2  23916  isclmp  25149  eulerpartlemn  34346  bnj976  34753  bnj543  34869  bnj594  34888  bnj917  34910  topdifinffinlem  37313  dath  39693  oeord2com  43273  ichexmpl1  47343  grtriproplem  47790  grtrif1o  47793  elfzolborelfzop1  48248  nnolog2flm1  48324  isthincd2  48705