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

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

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 1011

This theorem is referenced by:  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  limeq  4517  smoeq  6551  tfrlemi1  6593  tfr1onlemaccex  6609  tfrcllemaccex  6622  ereq1  6804  updjud  7412  ctssdclemr  7442  tapeq1  7608  tapeq2  7609  elinp  7831  sup3exmid  9277  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  fzaddel  10443  elfzomelpfzo  10627  seq3f1olemstep  10929  seq3f1olemp  10930  wrdl1s1  11376  sumeq1  12099  summodclem2  12127  summodc  12128  zsumdc  12129  prodmodclem2  12322  prodmodc  12323  divalglemnn  12663  divalglemeunn  12666  divalglemeuneg  12668  dfgcd2  12769  pythagtriplem18  13038  pythagtriplem19  13039  ctiunct  13309  ssomct  13314  isstruct2im  13340  isstruct2r  13341  ptex  13595  imasmnd2  13736  imasgrp2  13890  isrngd  14227  imasrng  14230  isringd  14319  imasring  14342  subrngpropd  14497  issubrg3  14528  islmod  14600  lmodlema  14601  islmodd  14602  lmodprop2d  14657  fiinopn  15028  lmfval  15217  upxp  15296  ivthdich  15677  2irrexpqap  16003  issubgr  16412  wksfval  16477  iswlk  16478  isclwwlk  16549  clwwlkn1loopb  16575  s2elclwwlknon2  16591  3dom  16932  dceqnconst  17015  dcapnconst  17016