Theorem 3anbi3i 1199

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

Syntax hints:   ↔ wb 198   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  cadcomb  1723  dfer2  7983  axgroth2  9935  oppgsubm  18104  xrsdsreclb  20115  ordthaus  21517  qtopeu  21848  regr1lem2  21872  isfbas2  21967  isclmp  23224  umgr2edg1  26444  xrge0adddir  30208  isros  30747  bnj964  31530  bnj1033  31554  dfon2lem7  32206  outsideofcom  32748  linecom  32770  linerflx2  32771  topdifinffinlem  33693  rdgeqoa  33716  ishlat2  35374  lhpex2leN  36034  lmbr3v  40721  lmbr3  40723  fourierdlem103  41169  fourierdlem104  41170  issmf  41683  issmff  41689  issmfle  41700  issmfgt  41711  issmfge  41724