Theorem 3anbi3d 1359

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi3d	⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		biidd 172	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1355	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  vtocl3gaf  2892  mob  3008  ordsoexmid  4711  tfr1onlemaccex  6623  tfrcllemaccex  6636  fseq1m1p1  10519  pfxsuff1eqwrdeq  11493  summodc  12175  fsum3  12179  divalglemnn  12710  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  mhmlem  13976  ring1  14471  lmodlema  14737  ivthreinc  15871  dvmptfsum  15951