Theorem 3anbi3i 1156

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

Syntax hints:   ↔ wb 205   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  cadcomb  1607  dfwrecsOLD  8328  dfer2  8735  ttrclresv  9760  axgroth2  10868  oppgsubm  19359  xrsdsreclb  21410  ordthaus  23379  qtopeu  23711  regr1lem2  23735  isfbas2  23830  isclmp  25115  umgr2edg1  29147  xrge0adddir  32901  isros  34001  bnj964  34788  bnj1033  34814  cusgr3cyclex  34964  dfon2lem7  35613  outsideofcom  35952  linecom  35974  linerflx2  35975  topdifinffinlem  37054  rdgeqoa  37077  ishlat2  39051  lhpex2leN  39712  aks6d1c1rh  41823  sn-isghm  42327  lmbr3v  45366  lmbr3  45368  fourierdlem103  45830  fourierdlem104  45831  issmf  46349  issmff  46355  issmfle  46366  issmfgt  46377  issmfge  46391  funcf2lem  48339