Theorem 3anbi3i 1176

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

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

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 401  df-3an 1104

This theorem is used by:  cadcomb  1642  dfer2  8693  ttrclresv  9684  axgroth2  10816  oppgsubm  19438  xrsdsreclb  21575  ordthaus  23552  qtopeu  23884  regr1lem2  23908  isfbas2  24003  isclmp  25267  umgr2edg1  29572  xrge0adddir  33347  isros  34567  bnj964  35340  bnj1033  35366  cusgr3cyclex  35636  dfon2lem7  36287  outsideofcom  36628  linecom  36650  linerflx2  36651  topdifinffinlem  38021  rdgeqoa  38044  ishlat2  40155  lhpex2leN  40815  aks6d1c1rh  42920  sn-isghm  43433  lmbr3v  46487  lmbr3  46489  fourierdlem103  46951  fourierdlem104  46952  issmf  47470  issmff  47476  issmfle  47487  issmfgt  47498  issmfge  47512  grtriproplem  48732  grtrif1o  48735  funcf2lem  49887