Theorem 3anbi3i 1157

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 1153	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  cadcomb  1616  dfwrecsOLD  8100  dfer2  8457  axgroth2  10512  oppgsubm  18884  xrsdsreclb  20557  ordthaus  22443  qtopeu  22775  regr1lem2  22799  isfbas2  22894  isclmp  24166  umgr2edg1  27481  xrge0adddir  31203  isros  32036  bnj964  32823  bnj1033  32849  cusgr3cyclex  32998  dfon2lem7  33671  ttrclresv  33703  outsideofcom  34357  linecom  34379  linerflx2  34380  topdifinffinlem  35445  rdgeqoa  35468  ishlat2  37294  lhpex2leN  37954  lmbr3v  43176  lmbr3  43178  fourierdlem103  43640  fourierdlem104  43641  issmf  44151  issmff  44157  issmfle  44168  issmfgt  44179  issmfge  44192  funcf2lem  46187