Theorem 3anbi123d 1349

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

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

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 1007

This theorem is referenced by:  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  limeq  4503  smoeq  6534  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  ereq1  6787  updjud  7386  ctssdclemr  7416  tapeq1  7582  tapeq2  7583  elinp  7805  sup3exmid  9248  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzaddel  10414  elfzomelpfzo  10598  seq3f1olemstep  10900  seq3f1olemp  10901  wrdl1s1  11343  sumeq1  12065  summodclem2  12093  summodc  12094  zsumdc  12095  prodmodclem2  12288  prodmodc  12289  divalglemnn  12629  divalglemeunn  12632  divalglemeuneg  12634  dfgcd2  12735  pythagtriplem18  13004  pythagtriplem19  13005  ctiunct  13275  ssomct  13280  isstruct2im  13306  isstruct2r  13307  ptex  13561  imasmnd2  13707  imasgrp2  13863  isrngd  14192  imasrng  14195  isringd  14284  imasring  14307  subrngpropd  14462  issubrg3  14493  islmod  14565  lmodlema  14566  islmodd  14567  lmodprop2d  14622  fiinopn  14995  lmfval  15184  upxp  15263  ivthdich  15644  2irrexpqap  15969  issubgr  16378  wksfval  16443  iswlk  16444  isclwwlk  16515  clwwlkn1loopb  16541  s2elclwwlknon2  16557  3dom  16888  dceqnconst  16972  dcapnconst  16973