Theorem 3anbi123d 1346

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi3d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))
bi3d.3	⊢ (𝜑 → (𝜂 ↔ 𝜁))

Assertion

Ref	Expression
3anbi123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 473	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 473	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1004	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1004	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  limeq  4468  smoeq  6442  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  ereq1  6695  updjud  7260  ctssdclemr  7290  tapeq1  7449  tapeq2  7450  elinp  7672  sup3exmid  9115  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  elfzomelpfzo  10449  seq3f1olemstep  10748  seq3f1olemp  10749  wrdl1s1  11178  sumeq1  11881  summodclem2  11908  summodc  11909  zsumdc  11910  prodmodclem2  12103  prodmodc  12104  divalglemnn  12444  divalglemeunn  12447  divalglemeuneg  12449  dfgcd2  12550  pythagtriplem18  12819  pythagtriplem19  12820  ctiunct  13026  ssomct  13031  isstruct2im  13057  isstruct2r  13058  ptex  13312  imasmnd2  13500  imasgrp2  13662  isrngd  13931  imasrng  13934  isringd  14019  imasring  14042  subrngpropd  14195  issubrg3  14226  islmod  14270  lmodlema  14271  islmodd  14272  lmodprop2d  14327  fiinopn  14693  lmfval  14882  upxp  14961  ivthdich  15342  2irrexpqap  15667  wksfval  16063  iswlk  16064  isclwwlk  16132  3dom  16411  dceqnconst  16488  dcapnconst  16489