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  dfwrecsOLD  8317  dfer2  8725  ttrclresv  9736  axgroth2  10844  oppgsubm  19350  xrsdsreclb  21386  ordthaus  23327  qtopeu  23659  regr1lem2  23683  isfbas2  23778  isclmp  25053  umgr2edg1  29195  xrge0adddir  33018  isros  34204  bnj964  34979  bnj1033  35005  cusgr3cyclex  35163  dfon2lem7  35812  outsideofcom  36151  linecom  36173  linerflx2  36174  topdifinffinlem  37370  rdgeqoa  37393  ishlat2  39376  lhpex2leN  40037  aks6d1c1rh  42143  sn-isghm  42663  lmbr3v  45741  lmbr3  45743  fourierdlem103  46205  fourierdlem104  46206  issmf  46724  issmff  46730  issmfle  46741  issmfgt  46752  issmfge  46766  grtriproplem  47918  grtrif1o  47921  funcf2lem  49013