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  1645  dfer2  8718  ttrclresv  9718  axgroth2  10910  oppgsubm  19576  xrsdsreclb  21720  ordthaus  23702  qtopeu  24035  regr1lem2  24059  isfbas2  24154  isclmp  25418  umgr2edg1  29792  xrge0adddir  33579  isros  34801  bnj964  35573  bnj1033  35599  cusgr3cyclex  35911  dfon2lem7  36551  outsideofcom  36893  linecom  36915  linerflx2  36916  topdifinffinlem  38271  rdgeqoa  38294  ishlat2  40411  lhpex2leN  41071  aks6d1c1rh  43176  sn-isghm  43685  lmbr3v  46755  lmbr3  46757  fourierdlem103  47219  fourierdlem104  47220  issmf  47738  issmff  47744  issmfle  47755  issmfgt  47766  issmfge  47780  grtriproplem  49037  grtrif1o  49040  funcf2lem  50189