Theorem 3anbi12d 1440

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 1439	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  1443  3anbi2d  1444  f1dom3el3dif  7218  xpord2pred  8089  fseq1m1p1  13547  dfrtrcl2  15018  imasdsval  17473  iscatd2  17641  ispos  18274  psgnunilem1  19462  rngpropd  20149  ringpropd  20263  mdetunilem3  22592  mdetunilem9  22598  dvfsumlem2  26007  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  istrkge  28542  axtg5seg  28550  axtgeucl  28557  iscgrad  28896  axlowdim  29047  axeuclid  29049  eengtrkge  29073  umgrvad2edg  29299  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  lt2addrd  32841  xlt2addrd  32850  constrsuc  33901  constrconj  33908  constrcccllem  33917  constrcbvlem  33918  sigaval  34274  issgon  34286  brafs  34835  loop1cycl  35338  brofs  36206  funtransport  36232  fvtransport  36233  brifs  36244  ifscgr  36245  brcgr3  36247  cgr3permute3  36248  brfs  36280  btwnconn1lem11  36298  funray  36341  fvray  36342  funline  36343  fvline  36345  lpolsetN  41945  rmydioph  43463  tfsconcatrev  43797  iunrelexpmin2  44160  fundcmpsurinj  47884  ichexmpl1  47944  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  isubgr3stgrlem4  48460  grlimgrtri  48494  iscnrm3r  49438  iscnrm3l  49441