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  7247  xpord2pred  8127  fseq1m1p1  13567  dfrtrcl2  15035  imasdsval  17485  iscatd2  17649  ispos  18282  psgnunilem1  19430  rngpropd  20090  ringpropd  20204  mdetunilem3  22508  mdetunilem9  22514  dvfsumlem2  25940  dvfsumlem2OLD  25941  istrkge  28391  axtg5seg  28399  axtgeucl  28406  iscgrad  28745  axlowdim  28895  axeuclid  28897  eengtrkge  28921  umgrvad2edg  29147  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  lt2addrd  32681  xlt2addrd  32689  constrsuc  33735  constrconj  33742  constrcccllem  33751  constrcbvlem  33752  sigaval  34108  issgon  34120  brafs  34670  loop1cycl  35131  brofs  36000  funtransport  36026  fvtransport  36027  brifs  36038  ifscgr  36039  brcgr3  36041  cgr3permute3  36042  brfs  36074  btwnconn1lem11  36092  funray  36135  fvray  36136  funline  36137  fvline  36139  lpolsetN  41483  rmydioph  43010  tfsconcatrev  43344  iunrelexpmin2  43708  fundcmpsurinj  47414  ichexmpl1  47474  cycl3grtri  47950  grimgrtri  47952  usgrgrtrirex  47953  isubgr3stgrlem4  47972  grlimgrtri  47999  iscnrm3r  48940  iscnrm3l  48943