Theorem 3anbi3d 1355

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

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

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 1007

This theorem is referenced by:  ceqsex3v  2857  ceqsex4v  2858  ceqsex8v  2860  vtocl3gaf  2884  mob  2999  ordsoexmid  4684  tfr1onlemaccex  6579  tfrcllemaccex  6592  fseq1m1p1  10429  pfxsuff1eqwrdeq  11391  summodc  12069  fsum3  12073  divalglemnn  12604  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  mhmlem  13831  ring1  14203  lmodlema  14440  ivthreinc  15510  dvmptfsum  15590