Theorem 3anbi12d 1445

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anbi1d  1448  3anbi2d  1449  f1dom3el3dif  7213  xpord2pred  8085  fseq1m1p1  13544  dfrtrcl2  15015  imasdsval  17470  iscatd2  17638  ispos  18271  psgnunilem1  19459  rngpropd  20146  ringpropd  20260  mdetunilem3  22597  mdetunilem9  22603  dvfsumlem2  26012  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  istrkge  28543  axtg5seg  28551  axtgeucl  28558  iscgrad  28897  axlowdim  29048  axeuclid  29050  eengtrkge  29074  umgrvad2edg  29300  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  lt2addrd  32842  xlt2addrd  32851  constrsuc  33922  constrconj  33929  constrcccllem  33938  constrcbvlem  33939  sigaval  34295  issgon  34307  brafs  34856  loop1cycl  35365  brofs  36233  funtransport  36259  fvtransport  36260  brifs  36271  ifscgr  36272  brcgr3  36274  cgr3permute3  36275  brfs  36307  btwnconn1lem11  36325  funray  36368  fvray  36369  funline  36370  fvline  36372  lpolsetN  41974  rmydioph  43459  tfsconcatrev  43793  iunrelexpmin2  44156  fundcmpsurinj  47884  ichexmpl1  47944  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  isubgr3stgrlem4  48460  grlimgrtri  48494  iscnrm3r  49438  iscnrm3l  49441