Theorem 3anbi1i 1246

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

Syntax hints:   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  iinfi  8206  fzolb  12345  brfi1uzind  13135  opfi1uzind  13138  brfi1uzindOLD  13141  opfi1uzindOLD  13144  sqrlem5  13835  bitsmod  14996  isfunc  16347  txcn  21239  trfil2  21501  isclmp  22705  eulerpartlemn  29770  bnj976  30102  bnj543  30217  bnj594  30236  bnj917  30258  topdifinffinlem  32371  dath  34040  elfzolborelfzop1  42103  nnolog2flm1  42182