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  7213  xpord2pred  8085  fseq1m1p1  13513  dfrtrcl2  14983  imasdsval  17434  iscatd2  17602  ispos  18235  psgnunilem1  19420  rngpropd  20107  ringpropd  20221  mdetunilem3  22556  mdetunilem9  22562  dvfsumlem2  25987  dvfsumlem2OLD  25988  istrkge  28478  axtg5seg  28486  axtgeucl  28493  iscgrad  28832  axlowdim  28983  axeuclid  28985  eengtrkge  29009  umgrvad2edg  29235  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  lt2addrd  32779  xlt2addrd  32788  constrsuc  33844  constrconj  33851  constrcccllem  33860  constrcbvlem  33861  sigaval  34217  issgon  34229  brafs  34778  loop1cycl  35280  brofs  36148  funtransport  36174  fvtransport  36175  brifs  36186  ifscgr  36187  brcgr3  36189  cgr3permute3  36190  brfs  36222  btwnconn1lem11  36240  funray  36283  fvray  36284  funline  36285  fvline  36287  lpolsetN  41681  rmydioph  43198  tfsconcatrev  43532  iunrelexpmin2  43895  fundcmpsurinj  47597  ichexmpl1  47657  cycl3grtri  48135  grimgrtri  48137  usgrgrtrirex  48138  isubgr3stgrlem4  48157  grlimgrtri  48191  iscnrm3r  49135  iscnrm3l  49138