Theorem 3anbi3i 1160

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 1156	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  cadcomb  1615  dfer2  8648  ttrclresv  9640  axgroth2  10750  oppgsubm  19308  xrsdsreclb  21385  ordthaus  23345  qtopeu  23677  regr1lem2  23701  isfbas2  23796  isclmp  25070  umgr2edg1  29302  xrge0adddir  33117  isros  34352  bnj964  35125  bnj1033  35151  cusgr3cyclex  35358  dfon2lem7  36009  outsideofcom  36350  linecom  36372  linerflx2  36373  topdifinffinlem  37629  rdgeqoa  37652  ishlat2  39758  lhpex2leN  40418  aks6d1c1rh  42524  sn-isghm  43060  lmbr3v  46132  lmbr3  46134  fourierdlem103  46596  fourierdlem104  46597  issmf  47115  issmff  47121  issmfle  47132  issmfgt  47143  issmfge  47157  grtriproplem  48328  grtrif1o  48331  funcf2lem  49469