Theorem 3anbi12d 1465

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi1d  1468  3anbi2d  1469  f1dom3el3dif  7277  xpord2pred  8168  fseq1m1p1  13740  dfrtrcl2  15224  imasdsval  17696  iscatd2  17864  ispos  18497  psgnunilem1  19716  rngpropd  20405  ringpropd  20528  mdetunilem3  22938  mdetunilem9  22944  dvfsumlem2  26356  bdayfinbndcbv  28861  bdayfinbndlem1  28862  bdayfinbndlem2  28863  istrkge  28928  axtg5seg  28936  axtgeucl  28943  iscgrad  29327  axlowdim  29548  axeuclid  29550  eengtrkge  29574  umgrvad2edg  29803  loop1cycl  30753  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  lt2addrd  33392  xlt2addrd  33401  constrsuc  34420  constrconj  34427  constrcccllem  34436  constrcbvlem  34437  sigaval  34793  issgon  34805  brafs  35354  brofs  36866  funtransport  36892  fvtransport  36893  brifs  36904  ifscgr  36905  brcgr3  36907  cgr3permute3  36908  brfs  36940  btwnconn1lem11  36958  funray  37001  fvray  37002  funline  37003  fvline  37005  lpolsetN  42648  rmydioph  44130  tfsconcatrev  44459  iunrelexpmin2  44821  fundcmpsurinj  48599  ichexmpl1  48659  cycl3grtri  49153  grimgrtri  49155  usgrgrtrirex  49156  isubgr3stgrlem4  49175  grlimgrtri  49209  iscnrm3r  50170  iscnrm3l  50173