Theorem 3anbi123d 1353

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 477	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 477	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1011	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1011	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  limeq  4524  smoeq  6565  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  ereq1  6818  updjud  7428  ctssdclemr  7458  tapeq1  7624  tapeq2  7625  elinp  7847  sup3exmid  9295  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzaddel  10482  elfzomelpfzo  10666  seq3f1olemstep  10972  seq3f1olemp  10973  wrdl1s1  11420  sumeq1  12146  summodclem2  12174  summodc  12175  zsumdc  12176  prodmodclem2  12369  prodmodc  12370  divalglemnn  12710  divalglemeunn  12713  divalglemeuneg  12715  dfgcd2  12816  pythagtriplem18  13089  pythagtriplem19  13090  ctiunct  13389  ssomct  13394  isstruct2im  13420  isstruct2r  13421  ptex  13677  imasmnd2  13818  imasgrp2  13972  isrngd  14359  imasrng  14362  isringd  14453  imasring  14478  subrngpropd  14633  issubrg3  14664  islmod  14736  lmodlema  14737  islmodd  14738  lmodprop2d  14794  fiinopn  15230  lmfval  15419  upxp  15498  ivthdich  15879  2irrexpqap  16214  issubgr  16703  wksfval  16768  iswlk  16769  isclwwlk  16840  clwwlkn1loopb  16866  s2elclwwlknon2  16882  3dom  17223  dceqnconst  17317  dcapnconst  17318