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  7272  xpord2pred  8147  fseq1m1p1  13644  dfrtrcl2  15123  imasdsval  17591  iscatd2  17759  ispos  18392  psgnunilem1  19607  rngpropd  20296  ringpropd  20417  mdetunilem3  22821  mdetunilem9  22827  dvfsumlem2  26237  bdayfinbndcbv  28710  bdayfinbndlem1  28711  bdayfinbndlem2  28712  istrkge  28777  axtg5seg  28785  axtgeucl  28792  iscgrad  29173  axlowdim  29366  axeuclid  29368  eengtrkge  29392  umgrvad2edg  29621  loop1cycl  30571  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  lt2addrd  33165  xlt2addrd  33174  constrsuc  34192  constrconj  34199  constrcccllem  34208  constrcbvlem  34209  sigaval  34565  issgon  34577  brafs  35127  brofs  36534  funtransport  36560  fvtransport  36561  brifs  36572  ifscgr  36573  brcgr3  36575  cgr3permute3  36576  brfs  36608  btwnconn1lem11  36626  funray  36669  fvray  36670  funline  36671  fvline  36673  lpolsetN  42314  rmydioph  43799  tfsconcatrev  44133  iunrelexpmin2  44496  fundcmpsurinj  48216  ichexmpl1  48276  cycl3grtri  48770  grimgrtri  48772  usgrgrtrirex  48773  isubgr3stgrlem4  48792  grlimgrtri  48826  iscnrm3r  49783  iscnrm3l  49786