Theorem 3anbi1i 1171

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

Syntax hints:   ↔ wb 208   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  iinfi  9365  fzolb  13673  brfi1uzind  14523  opfi1uzind  14526  01sqrexlem5  15275  bitsmod  16472  isfunc  17899  txcn  23688  trfil2  23949  isclmp  25161  eulerpartlemn  34680  bnj976  35075  bnj543  35190  bnj594  35209  bnj917  35231  topdifinffinlem  37846  dath  40365  oeord2com  43893  ichexmpl1  48080  grtriproplem  48566  grtrif1o  48569  elfzolborelfzop1  49146  nnolog2flm1  49217  isthincd2  50063