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  7262  xpord2pred  8144  fseq1m1p1  13616  dfrtrcl2  15081  imasdsval  17529  iscatd2  17693  ispos  18326  psgnunilem1  19474  rngpropd  20134  ringpropd  20248  mdetunilem3  22552  mdetunilem9  22558  dvfsumlem2  25985  dvfsumlem2OLD  25986  istrkge  28436  axtg5seg  28444  axtgeucl  28451  iscgrad  28790  axlowdim  28940  axeuclid  28942  eengtrkge  28966  umgrvad2edg  29192  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  lt2addrd  32728  xlt2addrd  32736  constrsuc  33772  constrconj  33779  constrcccllem  33788  constrcbvlem  33789  sigaval  34142  issgon  34154  brafs  34704  loop1cycl  35159  brofs  36023  funtransport  36049  fvtransport  36050  brifs  36061  ifscgr  36062  brcgr3  36064  cgr3permute3  36065  brfs  36097  btwnconn1lem11  36115  funray  36158  fvray  36159  funline  36160  fvline  36162  lpolsetN  41501  rmydioph  43038  tfsconcatrev  43372  iunrelexpmin2  43736  fundcmpsurinj  47423  ichexmpl1  47483  cycl3grtri  47959  grimgrtri  47961  usgrgrtrirex  47962  isubgr3stgrlem4  47981  grlimgrtri  48008  iscnrm3r  48922  iscnrm3l  48925