Theorem 3anbi3i 1177

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cadcomb  1646  dfer2  8743  ttrclresv  9742  axgroth2  10934  oppgsubm  19603  xrsdsreclb  21747  ordthaus  23729  qtopeu  24062  regr1lem2  24086  isfbas2  24181  isclmp  25445  umgr2edg1  29819  xrge0adddir  33646  isros  34868  bnj964  35640  bnj1033  35666  cusgr3cyclex  36067  dfon2lem7  36728  outsideofcom  37070  linecom  37092  linerflx2  37093  topdifinffinlem  38461  rdgeqoa  38484  ishlat2  40601  lhpex2leN  41261  aks6d1c1rh  43366  sn-isghm  43875  lmbr3v  46958  lmbr3  46960  fourierdlem103  47422  fourierdlem104  47423  issmf  47941  issmff  47947  issmfle  47958  issmfgt  47969  issmfge  47983  grtriproplem  49240  grtrif1o  49243  funcf2lem  50398