Theorem 3anbi12d 1463

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anbi1d  1466  3anbi2d  1467  f1dom3el3dif  7268  xpord2pred  8140  fseq1m1p1  13626  dfrtrcl2  15098  imasdsval  17568  iscatd2  17736  ispos  18369  psgnunilem1  19562  rngpropd  20251  ringpropd  20370  mdetunilem3  22739  mdetunilem9  22745  dvfsumlem2  26154  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  istrkge  28691  axtg5seg  28699  axtgeucl  28706  iscgrad  29078  axlowdim  29251  axeuclid  29253  eengtrkge  29277  umgrvad2edg  29503  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  lt2addrd  33035  xlt2addrd  33044  constrsuc  34072  constrconj  34079  constrcccllem  34088  constrcbvlem  34089  sigaval  34445  issgon  34457  brafs  35006  loop1cycl  35527  brofs  36395  funtransport  36421  fvtransport  36422  brifs  36433  ifscgr  36434  brcgr3  36436  cgr3permute3  36437  brfs  36469  btwnconn1lem11  36487  funray  36530  fvray  36531  funline  36532  fvline  36534  lpolsetN  42145  rmydioph  43632  tfsconcatrev  43966  iunrelexpmin2  44329  fundcmpsurinj  48046  ichexmpl1  48106  cycl3grtri  48600  grimgrtri  48602  usgrgrtrirex  48603  isubgr3stgrlem4  48622  grlimgrtri  48656  iscnrm3r  49610  iscnrm3l  49613