Theorem 3anbi12d 1436

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3anbi1d  1439  3anbi2d  1440  f1dom3el3dif  7271  xpord2pred  8135  fseq1m1p1  13581  dfrtrcl2  15014  imasdsval  17466  iscatd2  17630  ispos  18272  psgnunilem1  19403  rngpropd  20069  ringpropd  20177  mdetunilem3  22337  mdetunilem9  22343  dvfsumlem2  25780  istrkge  27976  axtg5seg  27984  axtgeucl  27991  iscgrad  28330  axlowdim  28487  axeuclid  28489  eengtrkge  28513  umgrvad2edg  28738  upgr3v3e3cycl  29701  upgr4cycl4dv4e  29706  lt2addrd  32232  xlt2addrd  32239  sigaval  33408  issgon  33420  brafs  33983  loop1cycl  34427  brofs  35282  funtransport  35308  fvtransport  35309  brifs  35320  ifscgr  35321  brcgr3  35323  cgr3permute3  35324  brfs  35356  btwnconn1lem11  35374  funray  35417  fvray  35418  funline  35419  fvline  35421  gg-dvfsumlem2  35470  lpolsetN  40657  rmydioph  42056  tfsconcatrev  42401  iunrelexpmin2  42766  fundcmpsurinj  46376  ichexmpl1  46436  iscnrm3r  47669  iscnrm3l  47672