Theorem 3anbi12d 1458

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3anbi1d  1461  3anbi2d  1462  f1dom3el3dif  7253  xpord2pred  8125  fseq1m1p1  13604  dfrtrcl2  15075  imasdsval  17545  iscatd2  17713  ispos  18346  psgnunilem1  19533  rngpropd  20220  ringpropd  20334  mdetunilem3  22671  mdetunilem9  22677  dvfsumlem2  26086  bdayfinbndcbv  28556  bdayfinbndlem1  28557  bdayfinbndlem2  28558  istrkge  28623  axtg5seg  28631  axtgeucl  28638  iscgrad  29002  axlowdim  29159  axeuclid  29161  eengtrkge  29185  umgrvad2edg  29411  upgr3v3e3cycl  30379  upgr4cycl4dv4e  30384  lt2addrd  32949  xlt2addrd  32958  constrsuc  34032  constrconj  34039  constrcccllem  34048  constrcbvlem  34049  sigaval  34405  issgon  34417  brafs  34966  loop1cycl  35484  brofs  36352  funtransport  36378  fvtransport  36379  brifs  36390  ifscgr  36391  brcgr3  36393  cgr3permute3  36394  brfs  36426  btwnconn1lem11  36444  funray  36487  fvray  36488  funline  36489  fvline  36491  lpolsetN  42103  rmydioph  43588  tfsconcatrev  43922  iunrelexpmin2  44285  fundcmpsurinj  48012  ichexmpl1  48072  cycl3grtri  48566  grimgrtri  48568  usgrgrtrirex  48569  isubgr3stgrlem4  48588  grlimgrtri  48622  iscnrm3r  49566  iscnrm3l  49569