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  7198  xpord2pred  8070  fseq1m1p1  13494  dfrtrcl2  14964  imasdsval  17414  iscatd2  17582  ispos  18215  psgnunilem1  19400  rngpropd  20087  ringpropd  20201  mdetunilem3  22524  mdetunilem9  22530  dvfsumlem2  25955  dvfsumlem2OLD  25956  istrkge  28430  axtg5seg  28438  axtgeucl  28445  iscgrad  28784  axlowdim  28934  axeuclid  28936  eengtrkge  28960  umgrvad2edg  29186  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  lt2addrd  32726  xlt2addrd  32734  constrsuc  33743  constrconj  33750  constrcccllem  33759  constrcbvlem  33760  sigaval  34116  issgon  34128  brafs  34677  loop1cycl  35173  brofs  36039  funtransport  36065  fvtransport  36066  brifs  36077  ifscgr  36078  brcgr3  36080  cgr3permute3  36081  brfs  36113  btwnconn1lem11  36131  funray  36174  fvray  36175  funline  36176  fvline  36178  lpolsetN  41521  rmydioph  43047  tfsconcatrev  43381  iunrelexpmin2  43745  fundcmpsurinj  47440  ichexmpl1  47500  cycl3grtri  47978  grimgrtri  47980  usgrgrtrirex  47981  isubgr3stgrlem4  48000  grlimgrtri  48034  iscnrm3r  48979  iscnrm3l  48982