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  7271  xpord2pred  8155  fseq1m1p1  13726  dfrtrcl2  15208  imasdsval  17680  iscatd2  17848  ispos  18481  psgnunilem1  19700  rngpropd  20389  ringpropd  20512  mdetunilem3  22922  mdetunilem9  22928  dvfsumlem2  26340  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  istrkge  28912  axtg5seg  28920  axtgeucl  28927  iscgrad  29311  axlowdim  29532  axeuclid  29534  eengtrkge  29558  umgrvad2edg  29787  loop1cycl  30737  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  lt2addrd  33335  xlt2addrd  33344  constrsuc  34363  constrconj  34370  constrcccllem  34379  constrcbvlem  34380  sigaval  34736  issgon  34748  brafs  35297  brofs  36750  funtransport  36776  fvtransport  36777  brifs  36788  ifscgr  36789  brcgr3  36791  cgr3permute3  36792  brfs  36824  btwnconn1lem11  36842  funray  36885  fvray  36886  funline  36887  fvline  36889  lpolsetN  42519  rmydioph  44000  tfsconcatrev  44334  iunrelexpmin2  44697  fundcmpsurinj  48460  ichexmpl1  48520  cycl3grtri  49014  grimgrtri  49016  usgrgrtrirex  49017  isubgr3stgrlem4  49036  grlimgrtri  49070  iscnrm3r  50025  iscnrm3l  50028