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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anbi1d  1468  3anbi2d  1469  f1dom3el3dif  7267  xpord2pred  8137  fseq1m1p1  13623  dfrtrcl2  15095  imasdsval  17564  iscatd2  17732  ispos  18365  psgnunilem1  19558  rngpropd  20247  ringpropd  20367  mdetunilem3  22771  mdetunilem9  22777  dvfsumlem2  26186  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  istrkge  28726  axtg5seg  28734  axtgeucl  28741  iscgrad  29122  axlowdim  29311  axeuclid  29313  eengtrkge  29337  umgrvad2edg  29563  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  lt2addrd  33095  xlt2addrd  33104  constrsuc  34128  constrconj  34135  constrcccllem  34144  constrcbvlem  34145  sigaval  34501  issgon  34513  brafs  35062  loop1cycl  35629  brofs  36497  funtransport  36523  fvtransport  36524  brifs  36535  ifscgr  36536  brcgr3  36538  cgr3permute3  36539  brfs  36571  btwnconn1lem11  36589  funray  36632  fvray  36633  funline  36634  fvline  36636  lpolsetN  42256  rmydioph  43741  tfsconcatrev  44075  iunrelexpmin2  44438  fundcmpsurinj  48158  ichexmpl1  48218  cycl3grtri  48712  grimgrtri  48714  usgrgrtrirex  48715  isubgr3stgrlem4  48734  grlimgrtri  48768  iscnrm3r  49726  iscnrm3l  49729