Theorem 3anbi3d 1331

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

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

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 983

This theorem is referenced by:  ceqsex3v  2817  ceqsex4v  2818  ceqsex8v  2820  vtocl3gaf  2844  mob  2959  ordsoexmid  4623  tfr1onlemaccex  6452  tfrcllemaccex  6465  fseq1m1p1  10247  pfxsuff1eqwrdeq  11185  summodc  11779  fsum3  11783  divalglemnn  12314  divalglemeunn  12317  divalglemex  12318  divalglemeuneg  12319  mhmlem  13535  ring1  13906  lmodlema  14139  ivthreinc  15202  dvmptfsum  15282