Theorem 3anbi1i 1153

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 1151	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   ↔ wb 208   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  iinfi  8867  fzolb  13034  brfi1uzind  13846  opfi1uzind  13849  sqrlem5  14591  bitsmod  15768  isfunc  17117  txcn  22217  trfil2  22478  isclmp  23684  eulerpartlemn  31646  bnj976  32056  bnj543  32172  bnj594  32191  bnj917  32213  topdifinffinlem  34644  dath  36904  ichexmpl1  43716  elfzolborelfzop1  44659  nnolog2flm1  44735