Theorem 3anbi12d 1392

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anbi1d  1395  3anbi2d  1396  f1dom3el3dif  6426  fseq1m1p1  12284  dfrtrcl2  13650  imasdsval  15998  iscatd2  16165  ispos  16770  psgnunilem1  17736  ringpropd  18405  mdetunilem3  20239  mdetunilem9  20245  dvfsumlem2  23594  istrkge  25156  axtg5seg  25164  axtgeucl  25171  iscgrad  25503  axlowdim  25641  axeuclid  25643  eengtrkge  25666  lt2addrd  28903  xlt2addrd  28913  sigaval  29500  issgon  29513  brafs  30003  brofs  31282  funtransport  31308  fvtransport  31309  brifs  31320  ifscgr  31321  brcgr3  31323  cgr3permute3  31324  brfs  31356  btwnconn1lem11  31374  funray  31417  fvray  31418  funline  31419  fvline  31421  lpolsetN  35789  rmydioph  36599  iunrelexpmin2  37023  umgrvad2edg  40440  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352