Theorem 3anbi3i 1158

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  cadcomb  1615  dfwrecsOLD  8116  dfer2  8486  ttrclresv  9462  axgroth2  10591  oppgsubm  18979  xrsdsreclb  20655  ordthaus  22545  qtopeu  22877  regr1lem2  22901  isfbas2  22996  isclmp  24270  umgr2edg1  27588  xrge0adddir  31309  isros  32144  bnj964  32931  bnj1033  32957  cusgr3cyclex  33106  dfon2lem7  33773  outsideofcom  34438  linecom  34460  linerflx2  34461  topdifinffinlem  35526  rdgeqoa  35549  ishlat2  37375  lhpex2leN  38035  lmbr3v  43267  lmbr3  43269  fourierdlem103  43731  fourierdlem104  43732  issmf  44242  issmff  44248  issmfle  44259  issmfgt  44270  issmfge  44283  funcf2lem  46277