Theorem 3anbi3i 1156

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

Syntax hints:   ↔ wb 209   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  cadcomb  1615  dfer2  8273  axgroth2  10236  oppgsubm  18482  xrsdsreclb  20138  ordthaus  21989  qtopeu  22321  regr1lem2  22345  isfbas2  22440  isclmp  23702  umgr2edg1  27001  xrge0adddir  30726  isros  31537  bnj964  32325  bnj1033  32351  cusgr3cyclex  32496  dfon2lem7  33147  outsideofcom  33702  linecom  33724  linerflx2  33725  topdifinffinlem  34764  rdgeqoa  34787  ishlat2  36649  lhpex2leN  37309  lmbr3v  42387  lmbr3  42389  fourierdlem103  42851  fourierdlem104  42852  issmf  43362  issmff  43368  issmfle  43379  issmfgt  43390  issmfge  43403