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  8636  ttrclresv  9628  axgroth2  10738  oppgsubm  19293  xrsdsreclb  21370  ordthaus  23330  qtopeu  23662  regr1lem2  23686  isfbas2  23781  isclmp  25055  umgr2edg1  29265  xrge0adddir  33079  isros  34304  bnj964  35078  bnj1033  35104  cusgr3cyclex  35309  dfon2lem7  35960  outsideofcom  36301  linecom  36323  linerflx2  36324  topdifinffinlem  37521  rdgeqoa  37544  ishlat2  39648  lhpex2leN  40308  aks6d1c1rh  42414  sn-isghm  42953  lmbr3v  46026  lmbr3  46028  fourierdlem103  46490  fourierdlem104  46491  issmf  47009  issmff  47015  issmfle  47026  issmfgt  47037  issmfge  47051  grtriproplem  48222  grtrif1o  48225  funcf2lem  49363