Theorem 3anbi3i 1160

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

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  cadcomb  1615  dfer2  8644  ttrclresv  9638  axgroth2  10748  oppgsubm  19337  xrsdsreclb  21394  ordthaus  23349  qtopeu  23681  regr1lem2  23705  isfbas2  23800  isclmp  25064  umgr2edg1  29280  xrge0adddir  33078  isros  34312  bnj964  35085  bnj1033  35111  cusgr3cyclex  35318  dfon2lem7  35969  outsideofcom  36310  linecom  36332  linerflx2  36333  topdifinffinlem  37663  rdgeqoa  37686  ishlat2  39799  lhpex2leN  40459  aks6d1c1rh  42564  sn-isghm  43106  lmbr3v  46173  lmbr3  46175  fourierdlem103  46637  fourierdlem104  46638  issmf  47156  issmff  47162  issmfle  47173  issmfgt  47184  issmfge  47198  grtriproplem  48415  grtrif1o  48418  funcf2lem  49556