Theorem 3anbi12d 1437

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anbi1d  1440  3anbi2d  1441  f1dom3el3dif  7306  xpord2pred  8186  fseq1m1p1  13659  dfrtrcl2  15111  imasdsval  17575  iscatd2  17739  ispos  18384  psgnunilem1  19535  rngpropd  20201  ringpropd  20311  mdetunilem3  22641  mdetunilem9  22647  dvfsumlem2  26087  dvfsumlem2OLD  26088  istrkge  28483  axtg5seg  28491  axtgeucl  28498  iscgrad  28837  axlowdim  28994  axeuclid  28996  eengtrkge  29020  umgrvad2edg  29248  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  lt2addrd  32758  xlt2addrd  32765  constrsuc  33728  constrconj  33735  sigaval  34075  issgon  34087  brafs  34649  loop1cycl  35105  brofs  35969  funtransport  35995  fvtransport  35996  brifs  36007  ifscgr  36008  brcgr3  36010  cgr3permute3  36011  brfs  36043  btwnconn1lem11  36061  funray  36104  fvray  36105  funline  36106  fvline  36108  lpolsetN  41439  rmydioph  42971  tfsconcatrev  43310  iunrelexpmin2  43674  fundcmpsurinj  47283  ichexmpl1  47343  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  iscnrm3r  48628  iscnrm3l  48631