Theorem 3anbi12d 1440

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 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anbi1d  1443  3anbi2d  1444  f1dom3el3dif  7225  xpord2pred  8097  fseq1m1p1  13527  dfrtrcl2  14997  imasdsval  17448  iscatd2  17616  ispos  18249  psgnunilem1  19434  rngpropd  20121  ringpropd  20235  mdetunilem3  22570  mdetunilem9  22576  dvfsumlem2  26001  dvfsumlem2OLD  26002  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  istrkge  28541  axtg5seg  28549  axtgeucl  28556  iscgrad  28895  axlowdim  29046  axeuclid  29048  eengtrkge  29072  umgrvad2edg  29298  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  lt2addrd  32841  xlt2addrd  32850  constrsuc  33916  constrconj  33923  constrcccllem  33932  constrcbvlem  33933  sigaval  34289  issgon  34301  brafs  34850  loop1cycl  35353  brofs  36221  funtransport  36247  fvtransport  36248  brifs  36259  ifscgr  36260  brcgr3  36262  cgr3permute3  36263  brfs  36295  btwnconn1lem11  36313  funray  36356  fvray  36357  funline  36358  fvline  36360  lpolsetN  41858  rmydioph  43371  tfsconcatrev  43705  iunrelexpmin2  44068  fundcmpsurinj  47769  ichexmpl1  47829  cycl3grtri  48307  grimgrtri  48309  usgrgrtrirex  48310  isubgr3stgrlem4  48329  grlimgrtri  48363  iscnrm3r  49307  iscnrm3l  49310