Theorem 3anbi3i 1163

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

Syntax hints:   ↔ wb 196   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  cadcomb  1699  dfer2  7910  axgroth2  9837  oppgsubm  17990  xrsdsreclb  19993  ordthaus  21388  qtopeu  21719  regr1lem2  21743  isfbas2  21838  isclmp  23095  umgr2edg1  26300  xrge0adddir  29999  isros  30538  bnj964  31318  bnj1033  31342  dfon2lem7  31997  outsideofcom  32539  linecom  32561  linerflx2  32562  topdifinffinlem  33504  rdgeqoa  33527  ishlat2  35141  lhpex2leN  35800  lmbr3v  40478  lmbr3  40480  fourierdlem103  40927  fourierdlem104  40928  issmf  41441  issmff  41447  issmfle  41458  issmfgt  41469  issmfge  41482