Theorem 3anbi1i 1202

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

Syntax hints:   ↔ wb 198   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  iinfi  8593  fzolb  12772  brfi1uzind  13570  opfi1uzind  13573  sqrlem5  14365  bitsmod  15532  isfunc  16877  txcn  21801  trfil2  22062  isclmp  23267  eulerpartlemn  30989  bnj976  31395  bnj543  31510  bnj594  31529  bnj917  31551  topdifinffinlem  33741  dath  35812  elfzolborelfzop1  43157  nnolog2flm1  43232