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  8300  dfer2  8706  ttrclresv  9714  axgroth2  10822  oppgsubm  19270  xrsdsreclb  21192  ordthaus  23108  qtopeu  23440  regr1lem2  23464  isfbas2  23559  isclmp  24837  umgr2edg1  28723  xrge0adddir  32448  isros  33452  bnj964  34240  bnj1033  34266  cusgr3cyclex  34413  dfon2lem7  35053  outsideofcom  35392  linecom  35414  linerflx2  35415  topdifinffinlem  36531  rdgeqoa  36554  ishlat2  38526  lhpex2leN  39187  lmbr3v  44760  lmbr3  44762  fourierdlem103  45224  fourierdlem104  45225  issmf  45743  issmff  45749  issmfle  45760  issmfgt  45771  issmfge  45785  funcf2lem  47726