Theorem 3anbi12d 1433

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

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

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 1086

This theorem is referenced by:  3anbi1d  1436  3anbi2d  1437  f1dom3el3dif  7260  xpord2pred  8125  fseq1m1p1  13573  dfrtrcl2  15006  imasdsval  17460  iscatd2  17624  ispos  18269  psgnunilem1  19403  rngpropd  20069  ringpropd  20177  mdetunilem3  22438  mdetunilem9  22444  dvfsumlem2  25883  dvfsumlem2OLD  25884  istrkge  28177  axtg5seg  28185  axtgeucl  28192  iscgrad  28531  axlowdim  28688  axeuclid  28690  eengtrkge  28714  umgrvad2edg  28939  upgr3v3e3cycl  29902  upgr4cycl4dv4e  29907  lt2addrd  32433  xlt2addrd  32440  sigaval  33598  issgon  33610  brafs  34173  loop1cycl  34617  brofs  35472  funtransport  35498  fvtransport  35499  brifs  35510  ifscgr  35511  brcgr3  35513  cgr3permute3  35514  brfs  35546  btwnconn1lem11  35564  funray  35607  fvray  35608  funline  35609  fvline  35611  lpolsetN  40843  rmydioph  42242  tfsconcatrev  42587  iunrelexpmin2  42952  fundcmpsurinj  46562  ichexmpl1  46622  iscnrm3r  47769  iscnrm3l  47772