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  7215  xpord2pred  8087  fseq1m1p1  13515  dfrtrcl2  14985  imasdsval  17436  iscatd2  17604  ispos  18237  psgnunilem1  19422  rngpropd  20109  ringpropd  20223  mdetunilem3  22558  mdetunilem9  22564  dvfsumlem2  25989  dvfsumlem2OLD  25990  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  istrkge  28529  axtg5seg  28537  axtgeucl  28544  iscgrad  28883  axlowdim  29034  axeuclid  29036  eengtrkge  29060  umgrvad2edg  29286  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  lt2addrd  32830  xlt2addrd  32839  constrsuc  33895  constrconj  33902  constrcccllem  33911  constrcbvlem  33912  sigaval  34268  issgon  34280  brafs  34829  loop1cycl  35331  brofs  36199  funtransport  36225  fvtransport  36226  brifs  36237  ifscgr  36238  brcgr3  36240  cgr3permute3  36241  brfs  36273  btwnconn1lem11  36291  funray  36334  fvray  36335  funline  36336  fvline  36338  lpolsetN  41742  rmydioph  43256  tfsconcatrev  43590  iunrelexpmin2  43953  fundcmpsurinj  47655  ichexmpl1  47715  cycl3grtri  48193  grimgrtri  48195  usgrgrtrirex  48196  isubgr3stgrlem4  48215  grlimgrtri  48249  iscnrm3r  49193  iscnrm3l  49196