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

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  cadcomb  1610  dfwrecsOLD  8354  dfer2  8764  ttrclresv  9786  axgroth2  10894  oppgsubm  19405  xrsdsreclb  21454  ordthaus  23413  qtopeu  23745  regr1lem2  23769  isfbas2  23864  isclmp  25149  umgr2edg1  29246  xrge0adddir  33004  isros  34132  bnj964  34919  bnj1033  34945  cusgr3cyclex  35104  dfon2lem7  35753  outsideofcom  36092  linecom  36114  linerflx2  36115  topdifinffinlem  37313  rdgeqoa  37336  ishlat2  39309  lhpex2leN  39970  aks6d1c1rh  42082  sn-isghm  42628  lmbr3v  45666  lmbr3  45668  fourierdlem103  46130  fourierdlem104  46131  issmf  46649  issmff  46655  issmfle  46666  issmfgt  46677  issmfge  46691  grtriproplem  47790  grtrif1o  47793  funcf2lem  48685