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  8639  ttrclresv  9633  axgroth2  10743  oppgsubm  19332  xrsdsreclb  21407  ordthaus  23363  qtopeu  23695  regr1lem2  23719  isfbas2  23814  isclmp  25078  umgr2edg1  29298  xrge0adddir  33097  isros  34332  bnj964  35105  bnj1033  35131  cusgr3cyclex  35338  dfon2lem7  35989  outsideofcom  36330  linecom  36352  linerflx2  36353  topdifinffinlem  37683  rdgeqoa  37706  ishlat2  39819  lhpex2leN  40479  aks6d1c1rh  42584  sn-isghm  43126  lmbr3v  46197  lmbr3  46199  fourierdlem103  46661  fourierdlem104  46662  issmf  47180  issmff  47186  issmfle  47197  issmfgt  47208  issmfge  47222  grtriproplem  48433  grtrif1o  48436  funcf2lem  49574