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  8626  ttrclresv  9613  axgroth2  10719  oppgsubm  19241  xrsdsreclb  21320  ordthaus  23269  qtopeu  23601  regr1lem2  23625  isfbas2  23720  isclmp  24995  umgr2edg1  29160  xrge0adddir  32981  isros  34151  bnj964  34926  bnj1033  34952  cusgr3cyclex  35129  dfon2lem7  35783  outsideofcom  36122  linecom  36144  linerflx2  36145  topdifinffinlem  37341  rdgeqoa  37364  ishlat2  39352  lhpex2leN  40012  aks6d1c1rh  42118  sn-isghm  42666  lmbr3v  45746  lmbr3  45748  fourierdlem103  46210  fourierdlem104  46211  issmf  46729  issmff  46735  issmfle  46746  issmfgt  46757  issmfge  46771  grtriproplem  47943  grtrif1o  47946  funcf2lem  49086