Theorem 3anbi12d 1465

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 1464	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi1d  1468  3anbi2d  1469  f1dom3el3dif  7266  xpord2pred  8143  fseq1m1p1  13654  dfrtrcl2  15135  imasdsval  17601  iscatd2  17769  ispos  18402  psgnunilem1  19620  rngpropd  20309  ringpropd  20430  mdetunilem3  22836  mdetunilem9  22842  dvfsumlem2  26254  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  istrkge  28798  axtg5seg  28806  axtgeucl  28813  iscgrad  29197  axlowdim  29418  axeuclid  29420  eengtrkge  29444  umgrvad2edg  29673  loop1cycl  30623  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  lt2addrd  33221  xlt2addrd  33230  constrsuc  34248  constrconj  34255  constrcccllem  34264  constrcbvlem  34265  sigaval  34621  issgon  34633  brafs  35183  brofs  36585  funtransport  36611  fvtransport  36612  brifs  36623  ifscgr  36624  brcgr3  36626  cgr3permute3  36627  brfs  36659  btwnconn1lem11  36677  funray  36720  fvray  36721  funline  36722  fvline  36724  lpolsetN  42355  rmydioph  43855  tfsconcatrev  44189  iunrelexpmin2  44552  fundcmpsurinj  48309  ichexmpl1  48369  cycl3grtri  48863  grimgrtri  48865  usgrgrtrirex  48866  isubgr3stgrlem4  48885  grlimgrtri  48919  iscnrm3r  49874  iscnrm3l  49877