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  8675  ttrclresv  9677  axgroth2  10785  oppgsubm  19301  xrsdsreclb  21337  ordthaus  23278  qtopeu  23610  regr1lem2  23634  isfbas2  23729  isclmp  25004  umgr2edg1  29145  xrge0adddir  32966  isros  34165  bnj964  34940  bnj1033  34966  cusgr3cyclex  35130  dfon2lem7  35784  outsideofcom  36123  linecom  36145  linerflx2  36146  topdifinffinlem  37342  rdgeqoa  37365  ishlat2  39353  lhpex2leN  40014  aks6d1c1rh  42120  sn-isghm  42668  lmbr3v  45750  lmbr3  45752  fourierdlem103  46214  fourierdlem104  46215  issmf  46733  issmff  46739  issmfle  46750  issmfgt  46761  issmfge  46775  grtriproplem  47942  grtrif1o  47945  funcf2lem  49074