Theorem 3anbi3i 1158

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 1154	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  1610  dfwrecsOLD  8337  dfer2  8745  ttrclresv  9755  axgroth2  10863  oppgsubm  19396  xrsdsreclb  21449  ordthaus  23408  qtopeu  23740  regr1lem2  23764  isfbas2  23859  isclmp  25144  umgr2edg1  29243  xrge0adddir  33006  isros  34149  bnj964  34936  bnj1033  34962  cusgr3cyclex  35121  dfon2lem7  35771  outsideofcom  36110  linecom  36132  linerflx2  36133  topdifinffinlem  37330  rdgeqoa  37353  ishlat2  39335  lhpex2leN  39996  aks6d1c1rh  42107  sn-isghm  42660  lmbr3v  45701  lmbr3  45703  fourierdlem103  46165  fourierdlem104  46166  issmf  46684  issmff  46690  issmfle  46701  issmfgt  46712  issmfge  46726  grtriproplem  47844  grtrif1o  47847  funcf2lem  48811