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 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  1439  3anbi2d  1440  f1dom3el3dif  7289  xpord2pred  8169  fseq1m1p1  13636  dfrtrcl2  15098  imasdsval  17562  iscatd2  17726  ispos  18372  psgnunilem1  19526  rngpropd  20192  ringpropd  20302  mdetunilem3  22636  mdetunilem9  22642  dvfsumlem2  26082  dvfsumlem2OLD  26083  istrkge  28480  axtg5seg  28488  axtgeucl  28495  iscgrad  28834  axlowdim  28991  axeuclid  28993  eengtrkge  29017  umgrvad2edg  29245  upgr3v3e3cycl  30209  upgr4cycl4dv4e  30214  lt2addrd  32762  xlt2addrd  32769  constrsuc  33743  constrconj  33750  sigaval  34092  issgon  34104  brafs  34666  loop1cycl  35122  brofs  35987  funtransport  36013  fvtransport  36014  brifs  36025  ifscgr  36026  brcgr3  36028  cgr3permute3  36029  brfs  36061  btwnconn1lem11  36079  funray  36122  fvray  36123  funline  36124  fvline  36126  lpolsetN  41465  rmydioph  43003  tfsconcatrev  43338  iunrelexpmin2  43702  fundcmpsurinj  47334  ichexmpl1  47394  grimgrtri  47852  usgrgrtrirex  47853  isubgr3stgrlem4  47872  grlimgrtri  47899  iscnrm3r  48745  iscnrm3l  48748