Theorem 3anbi12d 1439

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 1438	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  1442  3anbi2d  1443  f1dom3el3dif  7289  xpord2pred  8170  fseq1m1p1  13639  dfrtrcl2  15101  imasdsval  17560  iscatd2  17724  ispos  18360  psgnunilem1  19511  rngpropd  20171  ringpropd  20285  mdetunilem3  22620  mdetunilem9  22626  dvfsumlem2  26067  dvfsumlem2OLD  26068  istrkge  28465  axtg5seg  28473  axtgeucl  28480  iscgrad  28819  axlowdim  28976  axeuclid  28978  eengtrkge  29002  umgrvad2edg  29230  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  lt2addrd  32755  xlt2addrd  32762  constrsuc  33779  constrconj  33786  sigaval  34112  issgon  34124  brafs  34687  loop1cycl  35142  brofs  36006  funtransport  36032  fvtransport  36033  brifs  36044  ifscgr  36045  brcgr3  36047  cgr3permute3  36048  brfs  36080  btwnconn1lem11  36098  funray  36141  fvray  36142  funline  36143  fvline  36145  lpolsetN  41484  rmydioph  43026  tfsconcatrev  43361  iunrelexpmin2  43725  fundcmpsurinj  47396  ichexmpl1  47456  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  isubgr3stgrlem4  47936  grlimgrtri  47963  iscnrm3r  48845  iscnrm3l  48848