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

Proof of Theorem 3anbi3i

Step	Hyp	Ref	Expression
1		biid 260	. 2 ⊢ (𝜒 ↔ 𝜒)
2		biid 260	. 2 ⊢ (𝜃 ↔ 𝜃)
3		3anbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	1, 2, 3	3anbi123i 1154	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  cadcomb  1615  dfwrecsOLD  8129  dfer2  8499  ttrclresv  9475  axgroth2  10581  oppgsubm  18969  xrsdsreclb  20645  ordthaus  22535  qtopeu  22867  regr1lem2  22891  isfbas2  22986  isclmp  24260  umgr2edg1  27578  xrge0adddir  31301  isros  32136  bnj964  32923  bnj1033  32949  cusgr3cyclex  33098  dfon2lem7  33765  outsideofcom  34430  linecom  34452  linerflx2  34453  topdifinffinlem  35518  rdgeqoa  35541  ishlat2  37367  lhpex2leN  38027  lmbr3v  43286  lmbr3  43288  fourierdlem103  43750  fourierdlem104  43751  issmf  44264  issmff  44270  issmfle  44281  issmfgt  44292  issmfge  44305  funcf2lem  46299