Theorem 3anbi3i 1175

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

Syntax hints:   ↔ wb 209   ∧ w3a 1101

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

This theorem is referenced by:  cadcomb  1640  dfer2  8695  ttrclresv  9686  axgroth2  10810  oppgsubm  19432  xrsdsreclb  21533  ordthaus  23510  qtopeu  23842  regr1lem2  23866  isfbas2  23961  isclmp  25225  umgr2edg1  29502  xrge0adddir  33279  isros  34503  bnj964  35276  bnj1033  35302  cusgr3cyclex  35561  dfon2lem7  36212  outsideofcom  36553  linecom  36575  linerflx2  36576  topdifinffinlem  37916  rdgeqoa  37939  ishlat2  40052  lhpex2leN  40712  aks6d1c1rh  42817  sn-isghm  43332  lmbr3v  46386  lmbr3  46388  fourierdlem103  46850  fourierdlem104  46851  issmf  47369  issmff  47375  issmfle  47386  issmfgt  47397  issmfge  47411  grtriproplem  48628  grtrif1o  48631  funcf2lem  49779