Theorem 3anbi12d 1548

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

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

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 383  df-3an 1073

This theorem is referenced by:  3anbi1d  1551  3anbi2d  1552  f1dom3el3dif  6668  fseq1m1p1  12618  dfrtrcl2  14006  imasdsval  16379  iscatd2  16545  ispos  17151  psgnunilem1  18116  ringpropd  18786  mdetunilem3  20634  mdetunilem9  20640  dvfsumlem2  24006  istrkge  25573  axtg5seg  25581  axtgeucl  25588  iscgrad  25920  axlowdim  26058  axeuclid  26060  eengtrkge  26083  umgrvad2edg  26323  upgr3v3e3cycl  27356  upgr4cycl4dv4e  27361  lt2addrd  29852  xlt2addrd  29859  sigaval  30509  issgon  30522  brafs  31086  etasslt  32253  brofs  32445  funtransport  32471  fvtransport  32472  brifs  32483  ifscgr  32484  brcgr3  32486  cgr3permute3  32487  brfs  32519  btwnconn1lem11  32537  funray  32580  fvray  32581  funline  32582  fvline  32584  lpolsetN  37289  rmydioph  38104  iunrelexpmin2  38527