Theorem 3anbi12d 1440

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anbi1d  1443  3anbi2d  1444  f1dom3el3dif  7224  xpord2pred  8095  fseq1m1p1  13553  dfrtrcl2  15024  imasdsval  17479  iscatd2  17647  ispos  18280  psgnunilem1  19468  rngpropd  20155  ringpropd  20269  mdetunilem3  22579  mdetunilem9  22585  dvfsumlem2  25994  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  istrkge  28525  axtg5seg  28533  axtgeucl  28540  iscgrad  28879  axlowdim  29030  axeuclid  29032  eengtrkge  29056  umgrvad2edg  29282  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  lt2addrd  32823  xlt2addrd  32832  constrsuc  33882  constrconj  33889  constrcccllem  33898  constrcbvlem  33899  sigaval  34255  issgon  34267  brafs  34816  loop1cycl  35319  brofs  36187  funtransport  36213  fvtransport  36214  brifs  36225  ifscgr  36226  brcgr3  36228  cgr3permute3  36229  brfs  36261  btwnconn1lem11  36279  funray  36322  fvray  36323  funline  36324  fvline  36326  lpolsetN  41928  rmydioph  43442  tfsconcatrev  43776  iunrelexpmin2  44139  fundcmpsurinj  47869  ichexmpl1  47929  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  isubgr3stgrlem4  48445  grlimgrtri  48479  iscnrm3r  49423  iscnrm3l  49426