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 265	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
4	1, 2, 3	3anbi123d 1434	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ 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 210  df-an 400  df-3an 1087

This theorem is referenced by:  3anbi1d  1438  3anbi2d  1439  f1dom3el3dif  7026  fseq1m1p1  13045  dfrtrcl2  14483  imasdsval  16861  iscatd2  17025  ispos  17638  psgnunilem1  18703  ringpropd  19418  mdetunilem3  21329  mdetunilem9  21335  dvfsumlem2  24741  istrkge  26365  axtg5seg  26373  axtgeucl  26380  iscgrad  26719  axlowdim  26869  axeuclid  26871  eengtrkge  26895  umgrvad2edg  27117  upgr3v3e3cycl  28079  upgr4cycl4dv4e  28084  lt2addrd  30612  xlt2addrd  30619  sigaval  31612  issgon  31624  brafs  32185  loop1cycl  32629  xpord2pred  33361  brofs  33892  funtransport  33918  fvtransport  33919  brifs  33930  ifscgr  33931  brcgr3  33933  cgr3permute3  33934  brfs  33966  btwnconn1lem11  33984  funray  34027  fvray  34028  funline  34029  fvline  34031  lpolsetN  39094  rmydioph  40374  iunrelexpmin2  40832  fundcmpsurinj  44354  ichexmpl1  44414  iscnrm3r  45694  iscnrm3l  45697