Theorem 3anbi12d 1435

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses

Ref	Expression
3anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3anbi12d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

Proof of Theorem 3anbi12d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3		biidd 261	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
4	1, 2, 3	3anbi123d 1434	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anbi1d  1438  3anbi2d  1439  f1dom3el3dif  7123  fseq1m1p1  13260  dfrtrcl2  14701  imasdsval  17143  iscatd2  17307  ispos  17947  psgnunilem1  19016  ringpropd  19736  mdetunilem3  21671  mdetunilem9  21677  dvfsumlem2  25096  istrkge  26722  axtg5seg  26730  axtgeucl  26737  iscgrad  27076  axlowdim  27232  axeuclid  27234  eengtrkge  27258  umgrvad2edg  27483  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  lt2addrd  30976  xlt2addrd  30983  sigaval  31979  issgon  31991  brafs  32552  loop1cycl  32999  xpord2pred  33719  brofs  34234  funtransport  34260  fvtransport  34261  brifs  34272  ifscgr  34273  brcgr3  34275  cgr3permute3  34276  brfs  34308  btwnconn1lem11  34326  funray  34369  fvray  34370  funline  34371  fvline  34373  lpolsetN  39423  rmydioph  40752  iunrelexpmin2  41209  fundcmpsurinj  44749  ichexmpl1  44809  iscnrm3r  46130  iscnrm3l  46133