Theorem 3anbi1i 1156

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  iinfi  9455  fzolb  13702  brfi1uzind  14544  opfi1uzind  14547  01sqrexlem5  15282  bitsmod  16470  isfunc  17915  txcn  23650  trfil2  23911  isclmp  25144  eulerpartlemn  34363  bnj976  34770  bnj543  34886  bnj594  34905  bnj917  34927  topdifinffinlem  37330  dath  39719  oeord2com  43301  ichexmpl1  47394  grtriproplem  47844  grtrif1o  47847  elfzolborelfzop1  48365  nnolog2flm1  48440  isthincd2  48838