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 1086

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 1088

This theorem is referenced by:  3anbi1d  1442  3anbi2d  1443  f1dom3el3dif  7244  xpord2pred  8124  fseq1m1p1  13560  dfrtrcl2  15028  imasdsval  17478  iscatd2  17642  ispos  18275  psgnunilem1  19423  rngpropd  20083  ringpropd  20197  mdetunilem3  22501  mdetunilem9  22507  dvfsumlem2  25933  dvfsumlem2OLD  25934  istrkge  28384  axtg5seg  28392  axtgeucl  28399  iscgrad  28738  axlowdim  28888  axeuclid  28890  eengtrkge  28914  umgrvad2edg  29140  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  lt2addrd  32674  xlt2addrd  32682  constrsuc  33728  constrconj  33735  constrcccllem  33744  constrcbvlem  33745  sigaval  34101  issgon  34113  brafs  34663  loop1cycl  35124  brofs  35993  funtransport  36019  fvtransport  36020  brifs  36031  ifscgr  36032  brcgr3  36034  cgr3permute3  36035  brfs  36067  btwnconn1lem11  36085  funray  36128  fvray  36129  funline  36130  fvline  36132  lpolsetN  41476  rmydioph  43003  tfsconcatrev  43337  iunrelexpmin2  43701  fundcmpsurinj  47410  ichexmpl1  47470  cycl3grtri  47946  grimgrtri  47948  usgrgrtrirex  47949  isubgr3stgrlem4  47968  grlimgrtri  47995  iscnrm3r  48936  iscnrm3l  48939