Theorem 3anbi3i 1159

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  cadcomb  1614  dfer2  8623  ttrclresv  9607  axgroth2  10716  oppgsubm  19274  xrsdsreclb  21350  ordthaus  23299  qtopeu  23631  regr1lem2  23655  isfbas2  23750  isclmp  25024  umgr2edg1  29189  xrge0adddir  32999  isros  34181  bnj964  34955  bnj1033  34981  cusgr3cyclex  35180  dfon2lem7  35831  outsideofcom  36172  linecom  36194  linerflx2  36195  topdifinffinlem  37391  rdgeqoa  37414  ishlat2  39451  lhpex2leN  40111  aks6d1c1rh  42217  sn-isghm  42765  lmbr3v  45842  lmbr3  45844  fourierdlem103  46306  fourierdlem104  46307  issmf  46825  issmff  46831  issmfle  46842  issmfgt  46853  issmfge  46867  grtriproplem  48038  grtrif1o  48041  funcf2lem  49181