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  2847  ceqsex4v  2848  ceqsex8v  2850  vtocl3gaf  2874  mob  2989  ordsoexmid  4666  tfr1onlemaccex  6557  tfrcllemaccex  6570  fseq1m1p1  10375  pfxsuff1eqwrdeq  11329  summodc  12007  fsum3  12011  divalglemnn  12542  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  mhmlem  13764  ring1  14136  lmodlema  14371  ivthreinc  15439  dvmptfsum  15519