Theorem 3anbi3i 1177

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cadcomb  1646  dfer2  8697  ttrclresv  9696  axgroth2  10867  oppgsubm  19523  xrsdsreclb  21667  ordthaus  23649  qtopeu  23982  regr1lem2  24006  isfbas2  24101  isclmp  25365  umgr2edg1  29711  xrge0adddir  33498  isros  34720  bnj964  35493  bnj1033  35519  cusgr3cyclex  35826  dfon2lem7  36467  outsideofcom  36809  linecom  36831  linerflx2  36832  topdifinffinlem  38184  rdgeqoa  38207  ishlat2  40324  lhpex2leN  40984  aks6d1c1rh  43089  sn-isghm  43617  lmbr3v  46671  lmbr3  46673  fourierdlem103  47135  fourierdlem104  47136  issmf  47654  issmff  47660  issmfle  47671  issmfgt  47682  issmfge  47696  grtriproplem  48953  grtrif1o  48956  funcf2lem  50105