Theorem 3anbi3i 1248

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

Syntax hints:   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  cadcomb  1543  dfer2  7630  axgroth2  9526  oppgsubm  17615  xrsdsreclb  19612  ordthaus  20998  qtopeu  21329  regr1lem2  21353  isfbas2  21449  isclmp  22705  nbgrasym  25968  xrge0adddir  29023  isros  29558  bnj964  30267  bnj1033  30291  dfon2lem7  30938  outsideofcom  31405  linecom  31427  linerflx2  31428  topdifinffinlem  32371  rdgeqoa  32394  ishlat2  33658  lhpex2leN  34317  fourierdlem103  39102  fourierdlem104  39103  issmf  39614  issmff  39620  issmfle  39632  issmfgt  39643  issmfge  39656  umgr2edg1  40438