Theorem 3anbi12d 1437

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anbi1d  1440  3anbi2d  1441  f1dom3el3dif  7221  xpord2pred  8082  fseq1m1p1  13526  dfrtrcl2  14959  imasdsval  17411  iscatd2  17575  ispos  18217  psgnunilem1  19289  ringpropd  20020  mdetunilem3  22000  mdetunilem9  22006  dvfsumlem2  25428  istrkge  27462  axtg5seg  27470  axtgeucl  27477  iscgrad  27816  axlowdim  27973  axeuclid  27975  eengtrkge  27999  umgrvad2edg  28224  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  lt2addrd  31724  xlt2addrd  31731  sigaval  32799  issgon  32811  brafs  33374  loop1cycl  33818  brofs  34666  funtransport  34692  fvtransport  34693  brifs  34704  ifscgr  34705  brcgr3  34707  cgr3permute3  34708  brfs  34740  btwnconn1lem11  34758  funray  34801  fvray  34802  funline  34803  fvline  34805  lpolsetN  40018  rmydioph  41396  tfsconcatrev  41741  iunrelexpmin2  42106  fundcmpsurinj  45721  ichexmpl1  45781  iscnrm3r  47101  iscnrm3l  47104