Theorem 3anbi12d 1439

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

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

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 1088

This theorem is referenced by:  3anbi1d  1442  3anbi2d  1443  f1dom3el3dif  7206  xpord2pred  8078  fseq1m1p1  13502  dfrtrcl2  14969  imasdsval  17419  iscatd2  17587  ispos  18220  psgnunilem1  19372  rngpropd  20059  ringpropd  20173  mdetunilem3  22499  mdetunilem9  22505  dvfsumlem2  25931  dvfsumlem2OLD  25932  istrkge  28402  axtg5seg  28410  axtgeucl  28417  iscgrad  28756  axlowdim  28906  axeuclid  28908  eengtrkge  28932  umgrvad2edg  29158  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  lt2addrd  32694  xlt2addrd  32702  constrsuc  33705  constrconj  33712  constrcccllem  33721  constrcbvlem  33722  sigaval  34078  issgon  34090  brafs  34640  loop1cycl  35114  brofs  35983  funtransport  36009  fvtransport  36010  brifs  36021  ifscgr  36022  brcgr3  36024  cgr3permute3  36025  brfs  36057  btwnconn1lem11  36075  funray  36118  fvray  36119  funline  36120  fvline  36122  lpolsetN  41465  rmydioph  42991  tfsconcatrev  43325  iunrelexpmin2  43689  fundcmpsurinj  47397  ichexmpl1  47457  cycl3grtri  47935  grimgrtri  47937  usgrgrtrirex  47938  isubgr3stgrlem4  47957  grlimgrtri  47991  iscnrm3r  48936  iscnrm3l  48939