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  8649  ttrclresv  9646  axgroth2  10754  oppgsubm  19276  xrsdsreclb  21355  ordthaus  23304  qtopeu  23636  regr1lem2  23660  isfbas2  23755  isclmp  25030  umgr2edg1  29191  xrge0adddir  33002  isros  34151  bnj964  34926  bnj1033  34952  cusgr3cyclex  35116  dfon2lem7  35770  outsideofcom  36109  linecom  36131  linerflx2  36132  topdifinffinlem  37328  rdgeqoa  37351  ishlat2  39339  lhpex2leN  40000  aks6d1c1rh  42106  sn-isghm  42654  lmbr3v  45736  lmbr3  45738  fourierdlem103  46200  fourierdlem104  46201  issmf  46719  issmff  46725  issmfle  46736  issmfgt  46747  issmfge  46761  grtriproplem  47931  grtrif1o  47934  funcf2lem  49063