Theorem 3anbi12d 1549

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3anbi1d  1552  3anbi2d  1553  f1dom3el3dif  6690  fseq1m1p1  12628  dfrtrcl2  14021  imasdsval  16397  iscatd2  16563  ispos  17168  psgnunilem1  18133  ringpropd  18802  mdetunilem3  20642  mdetunilem9  20648  dvfsumlem2  24009  istrkge  25576  axtg5seg  25584  axtgeucl  25591  iscgrad  25923  axlowdim  26061  axeuclid  26063  eengtrkge  26086  umgrvad2edg  26325  upgr3v3e3cycl  27353  upgr4cycl4dv4e  27358  lt2addrd  29846  xlt2addrd  29853  sigaval  30503  issgon  30516  brafs  31080  etasslt  32247  brofs  32439  funtransport  32465  fvtransport  32466  brifs  32477  ifscgr  32478  brcgr3  32480  cgr3permute3  32481  brfs  32513  btwnconn1lem11  32531  funray  32574  fvray  32575  funline  32576  fvline  32578  lpolsetN  37291  rmydioph  38101  iunrelexpmin2  38524