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  8700  ttrclresv  9699  axgroth2  10837  oppgsubm  19490  xrsdsreclb  21628  ordthaus  23610  qtopeu  23943  regr1lem2  23967  isfbas2  24062  isclmp  25326  umgr2edg1  29657  xrge0adddir  33445  isros  34666  bnj964  35439  bnj1033  35465  cusgr3cyclex  35712  dfon2lem7  36353  outsideofcom  36695  linecom  36717  linerflx2  36718  topdifinffinlem  38088  rdgeqoa  38111  ishlat2  40213  lhpex2leN  40873  aks6d1c1rh  42978  sn-isghm  43506  lmbr3v  46560  lmbr3  46562  fourierdlem103  47024  fourierdlem104  47025  issmf  47543  issmff  47549  issmfle  47560  issmfgt  47571  issmfge  47585  grtriproplem  48842  grtrif1o  48845  funcf2lem  49994