Theorem 3anbi3i 1155

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

Proof of Theorem 3anbi3i

Step	Hyp	Ref	Expression
1		biid 263	. 2 ⊢ (𝜒 ↔ 𝜒)
2		biid 263	. 2 ⊢ (𝜃 ↔ 𝜃)
3		3anbi1i.1	. 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:  cadcomb  1610  dfer2  8284  axgroth2  10241  oppgsubm  18484  xrsdsreclb  20586  ordthaus  21986  qtopeu  22318  regr1lem2  22342  isfbas2  22437  isclmp  23695  umgr2edg1  26987  xrge0adddir  30674  isros  31422  bnj964  32210  bnj1033  32236  cusgr3cyclex  32378  dfon2lem7  33029  outsideofcom  33584  linecom  33606  linerflx2  33607  topdifinffinlem  34622  rdgeqoa  34645  ishlat2  36483  lhpex2leN  37143  lmbr3v  42018  lmbr3  42020  fourierdlem103  42487  fourierdlem104  42488  issmf  42998  issmff  43004  issmfle  43015  issmfgt  43026  issmfge  43039