Theorem 3anbi12d 1439

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anbi1d  1442  3anbi2d  1443  f1dom3el3dif  7206  xpord2pred  8078  fseq1m1p1  13502  dfrtrcl2  14969  imasdsval  17419  iscatd2  17587  ispos  18220  psgnunilem1  19372  rngpropd  20059  ringpropd  20173  mdetunilem3  22499  mdetunilem9  22505  dvfsumlem2  25931  dvfsumlem2OLD  25932  istrkge  28402  axtg5seg  28410  axtgeucl  28417  iscgrad  28756  axlowdim  28906  axeuclid  28908  eengtrkge  28932  umgrvad2edg  29158  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  lt2addrd  32694  xlt2addrd  32702  constrsuc  33705  constrconj  33712  constrcccllem  33721  constrcbvlem  33722  sigaval  34078  issgon  34090  brafs  34640  loop1cycl  35110  brofs  35979  funtransport  36005  fvtransport  36006  brifs  36017  ifscgr  36018  brcgr3  36020  cgr3permute3  36021  brfs  36053  btwnconn1lem11  36071  funray  36114  fvray  36115  funline  36116  fvline  36118  lpolsetN  41461  rmydioph  42987  tfsconcatrev  43321  iunrelexpmin2  43685  fundcmpsurinj  47393  ichexmpl1  47453  cycl3grtri  47931  grimgrtri  47933  usgrgrtrirex  47934  isubgr3stgrlem4  47953  grlimgrtri  47987  iscnrm3r  48932  iscnrm3l  48935