Theorem 3anbi3i 1160

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

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  cadcomb  1615  dfer2  8638  ttrclresv  9630  axgroth2  10740  oppgsubm  19295  xrsdsreclb  21372  ordthaus  23332  qtopeu  23664  regr1lem2  23688  isfbas2  23783  isclmp  25057  umgr2edg1  29288  xrge0adddir  33102  isros  34327  bnj964  35101  bnj1033  35127  cusgr3cyclex  35332  dfon2lem7  35983  outsideofcom  36324  linecom  36346  linerflx2  36347  topdifinffinlem  37554  rdgeqoa  37577  ishlat2  39681  lhpex2leN  40341  aks6d1c1rh  42447  sn-isghm  42983  lmbr3v  46056  lmbr3  46058  fourierdlem103  46520  fourierdlem104  46521  issmf  47039  issmff  47045  issmfle  47056  issmfgt  47067  issmfge  47081  grtriproplem  48252  grtrif1o  48255  funcf2lem  49393