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

Syntax hints:   ↔ wb 205   ∧ w3a 1087

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 1089

This theorem is referenced by:  cadcomb  1614  dfwrecsOLD  8249  dfer2  8656  ttrclresv  9662  axgroth2  10770  oppgsubm  19157  xrsdsreclb  20881  ordthaus  22772  qtopeu  23104  regr1lem2  23128  isfbas2  23223  isclmp  24497  umgr2edg1  28222  xrge0adddir  31953  isros  32856  bnj964  33644  bnj1033  33670  cusgr3cyclex  33817  dfon2lem7  34450  outsideofcom  34789  linecom  34811  linerflx2  34812  topdifinffinlem  35891  rdgeqoa  35914  ishlat2  37888  lhpex2leN  38549  lmbr3v  44106  lmbr3  44108  fourierdlem103  44570  fourierdlem104  44571  issmf  45089  issmff  45095  issmfle  45106  issmfgt  45117  issmfge  45131  funcf2lem  47158