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  1613  dfer2  8649  ttrclresv  9648  axgroth2  10756  oppgsubm  19277  xrsdsreclb  21356  ordthaus  23305  qtopeu  23637  regr1lem2  23661  isfbas2  23756  isclmp  25031  umgr2edg1  29192  xrge0adddir  33003  isros  34152  bnj964  34927  bnj1033  34953  cusgr3cyclex  35117  dfon2lem7  35771  outsideofcom  36110  linecom  36132  linerflx2  36133  topdifinffinlem  37329  rdgeqoa  37352  ishlat2  39340  lhpex2leN  40001  aks6d1c1rh  42107  sn-isghm  42655  lmbr3v  45737  lmbr3  45739  fourierdlem103  46201  fourierdlem104  46202  issmf  46720  issmff  46726  issmfle  46737  issmfgt  46748  issmfge  46762  grtriproplem  47932  grtrif1o  47935  funcf2lem  49064