Theorem 3anbi3d 1354

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

Syntax hints:   → wi 4   ↔ wb 105   ∧ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  vtocl3gaf  2873  mob  2988  ordsoexmid  4660  tfr1onlemaccex  6514  tfrcllemaccex  6527  fseq1m1p1  10330  pfxsuff1eqwrdeq  11284  summodc  11962  fsum3  11966  divalglemnn  12497  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  mhmlem  13719  ring1  14091  lmodlema  14325  ivthreinc  15388  dvmptfsum  15468