Theorem 3anbi3i 1166

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 263	. 2 ⊢ (𝜒 ↔ 𝜒)
2		biid 263	. 2 ⊢ (𝜃 ↔ 𝜃)
3		3anbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	1, 2, 3	3anbi123i 1162	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  cadcomb  1621  dfer2  8638  ttrclresv  9633  axgroth2  10743  oppgsubm  19332  xrsdsreclb  21393  ordthaus  23371  qtopeu  23703  regr1lem2  23727  isfbas2  23822  isclmp  25086  umgr2edg1  29302  xrge0adddir  33101  isros  34364  bnj964  35140  bnj1033  35166  cusgr3cyclex  35379  dfon2lem7  36030  outsideofcom  36371  linecom  36393  linerflx2  36394  topdifinffinlem  37724  rdgeqoa  37747  ishlat2  39860  lhpex2leN  40520  aks6d1c1rh  42625  sn-isghm  43138  lmbr3v  46202  lmbr3  46204  fourierdlem103  46666  fourierdlem104  46667  issmf  47185  issmff  47191  issmfle  47202  issmfgt  47213  issmfge  47227  grtriproplem  48444  grtrif1o  48447  funcf2lem  49585