Theorem 3anbi12d 1433

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anbi1d  1436  3anbi2d  1437  f1dom3el3dif  7029  fseq1m1p1  12985  dfrtrcl2  14423  imasdsval  16790  iscatd2  16954  ispos  17559  psgnunilem1  18623  ringpropd  19334  mdetunilem3  21225  mdetunilem9  21231  dvfsumlem2  24626  istrkge  26245  axtg5seg  26253  axtgeucl  26260  iscgrad  26599  axlowdim  26749  axeuclid  26751  eengtrkge  26775  umgrvad2edg  26997  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  lt2addrd  30477  xlt2addrd  30484  sigaval  31372  issgon  31384  brafs  31945  loop1cycl  32386  etasslt  33276  brofs  33468  funtransport  33494  fvtransport  33495  brifs  33506  ifscgr  33507  brcgr3  33509  cgr3permute3  33510  brfs  33542  btwnconn1lem11  33560  funray  33603  fvray  33604  funline  33605  fvline  33607  lpolsetN  38620  rmydioph  39618  iunrelexpmin2  40064  fundcmpsurinj  43576  ichexmpl1  43638