Theorem 3anbi3d 1352

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

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

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 1004

This theorem is referenced by:  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  vtocl3gaf  2870  mob  2985  ordsoexmid  4653  tfr1onlemaccex  6492  tfrcllemaccex  6505  fseq1m1p1  10287  pfxsuff1eqwrdeq  11226  summodc  11889  fsum3  11893  divalglemnn  12424  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  mhmlem  13646  ring1  14017  lmodlema  14250  ivthreinc  15313  dvmptfsum  15393