Theorem 3anbi3i 1159

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  cadcomb  1612  dfwrecsOLD  8339  dfer2  8747  ttrclresv  9758  axgroth2  10866  oppgsubm  19382  xrsdsreclb  21432  ordthaus  23393  qtopeu  23725  regr1lem2  23749  isfbas2  23844  isclmp  25131  umgr2edg1  29229  xrge0adddir  33024  isros  34170  bnj964  34958  bnj1033  34984  cusgr3cyclex  35142  dfon2lem7  35791  outsideofcom  36130  linecom  36152  linerflx2  36153  topdifinffinlem  37349  rdgeqoa  37372  ishlat2  39355  lhpex2leN  40016  aks6d1c1rh  42127  sn-isghm  42688  lmbr3v  45765  lmbr3  45767  fourierdlem103  46229  fourierdlem104  46230  issmf  46748  issmff  46754  issmfle  46765  issmfgt  46776  issmfge  46790  grtriproplem  47911  grtrif1o  47914  funcf2lem  48930