Theorem 3anbi3i 1173

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

Syntax hints:   ↔ wb 208   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  cadcomb  1635  dfer2  8681  ttrclresv  9674  axgroth2  10785  oppgsubm  19404  xrsdsreclb  21468  ordthaus  23446  qtopeu  23778  regr1lem2  23802  isfbas2  23897  isclmp  25161  umgr2edg1  29414  xrge0adddir  33198  isros  34467  bnj964  35240  bnj1033  35266  cusgr3cyclex  35491  dfon2lem7  36142  outsideofcom  36483  linecom  36505  linerflx2  36506  topdifinffinlem  37846  rdgeqoa  37869  ishlat2  39982  lhpex2leN  40642  aks6d1c1rh  42747  sn-isghm  43260  lmbr3v  46324  lmbr3  46326  fourierdlem103  46788  fourierdlem104  46789  issmf  47307  issmff  47313  issmfle  47324  issmfgt  47335  issmfge  47349  grtriproplem  48566  grtrif1o  48569  funcf2lem  49707