Theorem 3anbi12d 1466

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 265	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
4	1, 2, 3	3anbi123d 1465	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi1d  1469  3anbi2d  1470  f1dom3el3dif  7304  xpord2pred  8199  fseq1m1p1  13773  dfrtrcl2  15258  imasdsval  17737  iscatd2  17905  ispos  18538  psgnunilem1  19758  rngpropd  20447  ringpropd  20570  mdetunilem3  22984  mdetunilem9  22990  dvfsumlem2  26402  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  istrkge  28976  axtg5seg  28984  axtgeucl  28991  iscgrad  29375  axlowdim  29596  axeuclid  29598  eengtrkge  29622  umgrvad2edg  29851  loop1cycl  30801  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  lt2addrd  33438  xlt2addrd  33447  constrsuc  34481  constrconj  34488  constrcccllem  34497  constrcbvlem  34498  sigaval  34854  issgon  34866  brafs  35415  brofs  36985  funtransport  37011  fvtransport  37012  brifs  37023  ifscgr  37024  brcgr3  37026  cgr3permute3  37027  brfs  37059  btwnconn1lem11  37077  funray  37120  fvray  37121  funline  37122  fvline  37124  lpolsetN  42805  rmydioph  44287  tfsconcatrev  44611  iunrelexpmin2  44973  fundcmpsurinj  48764  ichexmpl1  48824  cycl3grtri  49318  grimgrtri  49320  usgrgrtrirex  49321  isubgr3stgrlem4  49340  grlimgrtri  49374  iscnrm3r  50393  iscnrm3l  50396