Theorem 3anbi1i 1158

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

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  iinfi  9324  fzolb  13614  brfi1uzind  14464  opfi1uzind  14467  01sqrexlem5  15202  bitsmod  16399  isfunc  17825  txcn  23604  trfil2  23865  isclmp  25077  eulerpartlemn  34544  bnj976  34939  bnj543  35054  bnj594  35073  bnj917  35095  topdifinffinlem  37680  dath  40199  oeord2com  43760  ichexmpl1  47944  grtriproplem  48430  grtrif1o  48433  elfzolborelfzop1  49010  nnolog2flm1  49081  isthincd2  49927