Theorem 3anbi13d 1430

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

Proof of Theorem 3anbi13d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 263	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1428	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3anbi3d  1434  ax12wdemo  2106  f1dom3el3dif  6892  wfrlem1  7805  wfrlem3a  7808  wfrlem15  7821  cofsmo  9537  axdc3lem3  9720  axdc3lem4  9721  iscatd2  16781  psgnunilem1  18352  nn0gsumfz  18821  opprsubrg  19246  lsspropd  19479  mdetunilem3  20907  mdetunilem9  20913  smadiadetr  20968  lmres  21592  cnhaus  21646  regsep2  21668  dishaus  21674  ordthauslem  21675  nconnsubb  21715  pthaus  21930  txhaus  21939  xkohaus  21945  regr1lem  22031  ustval  22494  methaus  22813  metnrmlem3  23152  pmltpclem1  23732  axtgeucl  25940  iscgrad  26279  dfcgra2  26298  f1otrge  26341  axeuclidlem  26431  umgrvad2edg  26678  elwspths2spth  27433  upgr3v3e3cycl  27646  upgr4cycl4dv4e  27651  vdgn1frgrv2  27767  numclwlk1lem1  27840  ex-opab  27903  isnvlem  28078  ajval  28329  adjeu  29357  adjval  29358  adj1  29401  adjeq  29403  cnlnssadj  29548  br8d  30051  lt2addrd  30163  xlt2addrd  30170  measval  31074  loop1cycl  31992  br8  32600  br6  32601  br4  32602  frrlem1  32732  frrlem13  32744  brsslt  32863  brcgr3  33116  brsegle  33178  fvray  33211  linedegen  33213  fvline  33214  poimirlem28  34451  isopos  35847  hlsuprexch  36048  2llnjN  36234  2lplnj  36287  cdlemk42  37608  zindbi  39028  jm2.27  39090  stoweidlem43  41870  fourierdlem42  41976  ichexmpl1  43113