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  7226  xpord2pred  8101  fseq1m1p1  13536  dfrtrcl2  15004  imasdsval  17454  iscatd2  17618  ispos  18251  psgnunilem1  19399  rngpropd  20059  ringpropd  20173  mdetunilem3  22477  mdetunilem9  22483  dvfsumlem2  25909  dvfsumlem2OLD  25910  istrkge  28360  axtg5seg  28368  axtgeucl  28375  iscgrad  28714  axlowdim  28864  axeuclid  28866  eengtrkge  28890  umgrvad2edg  29116  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  lt2addrd  32647  xlt2addrd  32655  constrsuc  33701  constrconj  33708  constrcccllem  33717  constrcbvlem  33718  sigaval  34074  issgon  34086  brafs  34636  loop1cycl  35097  brofs  35966  funtransport  35992  fvtransport  35993  brifs  36004  ifscgr  36005  brcgr3  36007  cgr3permute3  36008  brfs  36040  btwnconn1lem11  36058  funray  36101  fvray  36102  funline  36103  fvline  36105  lpolsetN  41449  rmydioph  42976  tfsconcatrev  43310  iunrelexpmin2  43674  fundcmpsurinj  47383  ichexmpl1  47443  cycl3grtri  47919  grimgrtri  47921  usgrgrtrirex  47922  isubgr3stgrlem4  47941  grlimgrtri  47968  iscnrm3r  48909  iscnrm3l  48912