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  8883  fzolb  13047  brfi1uzind  13859  opfi1uzind  13862  sqrlem5  14608  bitsmod  15787  isfunc  17136  txcn  22236  trfil2  22497  isclmp  23703  eulerpartlemn  31641  bnj976  32051  bnj543  32167  bnj594  32186  bnj917  32208  topdifinffinlem  34630  dath  36874  ichexmpl1  43638  elfzolborelfzop1  44581  nnolog2flm1  44657