Theorem 3anbi12d 1436

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anbi1d  1439  3anbi2d  1440  f1dom3el3dif  7151  fseq1m1p1  13340  dfrtrcl2  14782  imasdsval  17235  iscatd2  17399  ispos  18041  psgnunilem1  19110  ringpropd  19830  mdetunilem3  21772  mdetunilem9  21778  dvfsumlem2  25200  istrkge  26827  axtg5seg  26835  axtgeucl  26842  iscgrad  27181  axlowdim  27338  axeuclid  27340  eengtrkge  27364  umgrvad2edg  27589  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  lt2addrd  31083  xlt2addrd  31090  sigaval  32088  issgon  32100  brafs  32661  loop1cycl  33108  xpord2pred  33801  brofs  34316  funtransport  34342  fvtransport  34343  brifs  34354  ifscgr  34355  brcgr3  34357  cgr3permute3  34358  brfs  34390  btwnconn1lem11  34408  funray  34451  fvray  34452  funline  34453  fvline  34455  lpolsetN  39503  rmydioph  40843  iunrelexpmin2  41327  fundcmpsurinj  44872  ichexmpl1  44932  iscnrm3r  46253  iscnrm3l  46256