Theorem 3anbi3i 1247

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

Syntax hints:   ↔ wb 194   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  cadcomb  1542  dfer2  7607  axgroth2  9503  oppgsubm  17563  xrsdsreclb  19560  ordthaus  20945  qtopeu  21276  regr1lem2  21300  isfbas2  21396  isclmp  22652  nbgrasym  25761  xrge0adddir  28816  isros  29351  bnj964  30060  bnj1033  30084  dfon2lem7  30731  outsideofcom  31198  linecom  31220  linerflx2  31221  topdifinffinlem  32154  rdgeqoa  32177  ishlat2  33441  lhpex2leN  34100  fourierdlem103  38885  fourierdlem104  38886  issmf  39397  issmff  39403  issmfle  39415  issmfgt  39426  issmfge  39439  umgr2edg1  40419