Theorem 3anbi1i 1164

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

Syntax hints:   ↔ wb 208   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  iinfi  9324  fzolb  13615  brfi1uzind  14465  opfi1uzind  14468  01sqrexlem5  15203  bitsmod  16400  isfunc  17826  txcn  23613  trfil2  23874  isclmp  25086  eulerpartlemn  34577  bnj976  34975  bnj543  35090  bnj594  35109  bnj917  35131  topdifinffinlem  37724  dath  40243  oeord2com  43771  ichexmpl1  47958  grtriproplem  48444  grtrif1o  48447  elfzolborelfzop1  49024  nnolog2flm1  49095  isthincd2  49941