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 1086

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 1088

This theorem is referenced by:  cadcomb  1613  dfer2  8672  ttrclresv  9670  axgroth2  10778  oppgsubm  19294  xrsdsreclb  21330  ordthaus  23271  qtopeu  23603  regr1lem2  23627  isfbas2  23722  isclmp  24997  umgr2edg1  29138  xrge0adddir  32959  isros  34158  bnj964  34933  bnj1033  34959  cusgr3cyclex  35123  dfon2lem7  35777  outsideofcom  36116  linecom  36138  linerflx2  36139  topdifinffinlem  37335  rdgeqoa  37358  ishlat2  39346  lhpex2leN  40007  aks6d1c1rh  42113  sn-isghm  42661  lmbr3v  45743  lmbr3  45745  fourierdlem103  46207  fourierdlem104  46208  issmf  46726  issmff  46732  issmfle  46743  issmfgt  46754  issmfge  46768  grtriproplem  47938  grtrif1o  47941  funcf2lem  49070