Theorem 3anbi12d 1435

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3anbi1d  1438  3anbi2d  1439  f1dom3el3dif  7270  xpord2pred  8133  fseq1m1p1  13580  dfrtrcl2  15013  imasdsval  17465  iscatd2  17629  ispos  18271  psgnunilem1  19402  rngpropd  20068  ringpropd  20176  mdetunilem3  22336  mdetunilem9  22342  dvfsumlem2  25779  istrkge  27975  axtg5seg  27983  axtgeucl  27990  iscgrad  28329  axlowdim  28486  axeuclid  28488  eengtrkge  28512  umgrvad2edg  28737  upgr3v3e3cycl  29700  upgr4cycl4dv4e  29705  lt2addrd  32231  xlt2addrd  32238  sigaval  33407  issgon  33419  brafs  33982  loop1cycl  34426  brofs  35281  funtransport  35307  fvtransport  35308  brifs  35319  ifscgr  35320  brcgr3  35322  cgr3permute3  35323  brfs  35355  btwnconn1lem11  35373  funray  35416  fvray  35417  funline  35418  fvline  35420  gg-dvfsumlem2  35469  lpolsetN  40656  rmydioph  42055  tfsconcatrev  42400  iunrelexpmin2  42765  fundcmpsurinj  46375  ichexmpl1  46435  iscnrm3r  47668  iscnrm3l  47671