Theorem 3anbi123d 1348

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

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

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 1006

This theorem is referenced by:  3anbi12d  1349  3anbi13d  1350  3anbi23d  1351  limeq  4474  smoeq  6456  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  ereq1  6709  updjud  7281  ctssdclemr  7311  tapeq1  7471  tapeq2  7472  elinp  7694  sup3exmid  9137  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  elfzomelpfzo  10477  seq3f1olemstep  10777  seq3f1olemp  10778  wrdl1s1  11211  sumeq1  11933  summodclem2  11961  summodc  11962  zsumdc  11963  prodmodclem2  12156  prodmodc  12157  divalglemnn  12497  divalglemeunn  12500  divalglemeuneg  12502  dfgcd2  12603  pythagtriplem18  12872  pythagtriplem19  12873  ctiunct  13079  ssomct  13084  isstruct2im  13110  isstruct2r  13111  ptex  13365  imasmnd2  13553  imasgrp2  13715  isrngd  13985  imasrng  13988  isringd  14073  imasring  14096  subrngpropd  14249  issubrg3  14280  islmod  14324  lmodlema  14325  islmodd  14326  lmodprop2d  14381  fiinopn  14747  lmfval  14936  upxp  15015  ivthdich  15396  2irrexpqap  15721  issubgr  16127  wksfval  16192  iswlk  16193  isclwwlk  16264  clwwlkn1loopb  16290  s2elclwwlknon2  16306  3dom  16638  dceqnconst  16716  dcapnconst  16717