Theorem 3anbi12d 1429

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3anbi1d  1432  3anbi2d  1433  f1dom3el3dif  6892  fseq1m1p1  12832  dfrtrcl2  14255  imasdsval  16617  iscatd2  16781  ispos  17386  psgnunilem1  18352  ringpropd  19022  mdetunilem3  20907  mdetunilem9  20913  dvfsumlem2  24307  istrkge  25925  axtg5seg  25933  axtgeucl  25940  iscgrad  26279  axlowdim  26430  axeuclid  26432  eengtrkge  26456  umgrvad2edg  26678  upgr3v3e3cycl  27646  upgr4cycl4dv4e  27651  lt2addrd  30163  xlt2addrd  30170  sigaval  30987  issgon  30999  brafs  31560  loop1cycl  31992  etasslt  32883  brofs  33075  funtransport  33101  fvtransport  33102  brifs  33113  ifscgr  33114  brcgr3  33116  cgr3permute3  33117  brfs  33149  btwnconn1lem11  33167  funray  33210  fvray  33211  funline  33212  fvline  33214  lpolsetN  38149  rmydioph  39096  iunrelexpmin2  39542  ichexmpl1  43113